Login
Check-in [86dd5dbc21]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:3.5: A guest address space

Claim: mem/guest_space.cr builds a guest's address space with 3.2's builder. Second-stage tables map guest-physical RAM onto pages from 3.1. Phase 4 will load them; nothing does yet. - mem/pte_aarch64.cr gains PteAarch64Stage2. Guest RAM has MemAttr 0b1111 (normal write-back), S2AP 0b11, SH inner, AF and XN 0b00. Device memory has MemAttr 0b0001 and XN 0b11. - mem/pte_x86_64.cr gains PteX86_64Nested, 3.2's long-mode format with U/S on every entry. NX is cleared for guest RAM, which 3.3b's format would otherwise set. - GuestSpace is a Crystal class allocated on 3.4's heap. It takes guest RAM in one 3.1 allocation, zeroes it, and maps it whole at 0x40000000 on aarch64 and at 0 on x86_64, with nothing else mapped. - It holds the root and the register values Phase 4 will load: VTTBR_EL2 (VMID 0) and VTCR_EL2 (T0SZ 16, SL0 2 for a level-0 start, WBWA inner-shareable walks, 4 KiB granule, PS from PARange capped at 48 bits, RES1 bit 31) on Arm, and the nested CR3 on x86. A CPU reporting fewer than 44 physical address bits is refused, since SL0 2 needs that. - translate(gpa, length, host) returns 0 for an empty range, a wrapping one or one leaving guest RAM. Otherwise it gives the host address and the bytes left to the end of that 4 KiB page. - free returns the RAM and every table page to 3.1. - The shell's new guest_space command builds a 16 MiB space, walks each of its 4,096 pages back through the builder, translates one fixed address and frees the space. It refuses at a hosted prompt.

Passage: xv6 §3.6: "Each process has its own page table, and when xv6 switches between processes, it also changes page tables." Hailperin §7.5.2: "the VMM does another level of mapping, translating the virtual machine's 'physical' page frames into the truly physical page frames of the hardware."

Demonstration: - bin/glint-run aarch64 --type guest_space prints "Guest space: 16 MiB at 0x40000000, host 0x4000a000, 4096 pages walked; 0x40123000 -> 0x4012d000". The host address is the base plus 0x123000. --no-virtualization, at EL1, prints the same line. - bin/glint-run x86_64 --type guest_space prints "Guest space: 16 MiB at 0x0, host 0x1a0000, 4096 pages walked; 0x123000 -> 0x2c3000", again the base plus 0x123000. - Typing it twice in one boot works: the first space is freed before the second is built. A hosted prompt answers "guest_space: native mode only (firmware owns the page tables)". - 3.4's boots are unchanged: the heap native and hosted, cat, fault "write" and overflow. - crystal spec, with QEMU_SRC, UBOOT_SRC, ZEPHYR_SRC, GLINT_UBOOT_BUILD_DIR, GLINT_QEMU_X86_64 and GLINT_QEMU_AARCH64 set, passes 699 examples with 0 failures, 0 errors and 0 pending, and leaves TMPDIR empty. spec/guest_space_spec.cr checks both formats against hand-encoded literals and the VTCR_EL2 value with its cap and RES1 bit. It checks translate at every edge, that only the space's own zeroed RAM is mapped, that free returns 3.1's free count to where it was, and that allocation and builder failures are statuses that lose no pages. - crystal tool format --check passes.

Size: 266 non-spec lines added and 1 removed, against ~330; spec +126. Largest function: the nested PageTable#map, 1,296 bytes; Shell.guest_space is 1,037. Images: BOOTAA64.EFI 164,864 -> 168,960 bytes; BOOTX64.EFI 164,352 -> 172,544.

Review: - The first run, 36c11892, stopped with the model at capacity and left an unusable patch, mostly cache bitcode inside the tree. It wasn't applied. This is run 29624d71, from 6076f190, and the patch's SHA3 matched the node's record. - The command is guest_space, not the phase text's guest-space. Codex had changed the shell lexer to read a hyphen inside an identifier. That breaks P's rule that "Everything a person types to Glint is Crystal syntax": Crystal parses guest-space as guest - space. The reviewer dropped the lexer change, renamed the command, and corrected docs/phases/03-page-tables.md and the task to match. - Codex was right that "3.2's format plus U/S" would have left guest RAM non-executable under 3.3b's NX. The nested format clears NX for guest RAM. - Only the spec checks VTCR_EL2's RES1 bit 31; no source here states it and QEMU doesn't check it. - The reviewer ran every boot and the full suite. - Second run. Verdict: merge.

Downloads: Tarball | ZIP archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA3-256: 86dd5dbc21e380d341817d82402b4479d9e22fb98858fd5d1a4900d674bbbd0e
User & Date: glint-session 2026-10-30 02:55:06.127
Context
2026-10-30
02:55
Tutorial: 3.5 check-in: 437bb241ad user: glint-session tags: trunk
02:55
3.5: A guest address space

Claim: mem/guest_space.cr builds a guest's address space with 3.2's builder. Second-stage tables map guest-physical RAM onto pages from 3.1. Phase 4 will load them; nothing does yet. - mem/pte_aarch64.cr gains PteAarch64Stage2. Guest RAM has MemAttr 0b1111 (normal write-back), S2AP 0b11, SH inner, AF and XN 0b00. Device memory has MemAttr 0b0001 and XN 0b11. - mem/pte_x86_64.cr gains PteX86_64Nested, 3.2's long-mode format with U/S on every entry. NX is cleared for guest RAM, which 3.3b's format would otherwise set. - GuestSpace is a Crystal class allocated on 3.4's heap. It takes guest RAM in one 3.1 allocation, zeroes it, and maps it whole at 0x40000000 on aarch64 and at 0 on x86_64, with nothing else mapped. - It holds the root and the register values Phase 4 will load: VTTBR_EL2 (VMID 0) and VTCR_EL2 (T0SZ 16, SL0 2 for a level-0 start, WBWA inner-shareable walks, 4 KiB granule, PS from PARange capped at 48 bits, RES1 bit 31) on Arm, and the nested CR3 on x86. A CPU reporting fewer than 44 physical address bits is refused, since SL0 2 needs that. - translate(gpa, length, host) returns 0 for an empty range, a wrapping one or one leaving guest RAM. Otherwise it gives the host address and the bytes left to the end of that 4 KiB page. - free returns the RAM and every table page to 3.1. - The shell's new guest_space command builds a 16 MiB space, walks each of its 4,096 pages back through the builder, translates one fixed address and frees the space. It refuses at a hosted prompt.

Passage: xv6 §3.6: "Each process has its own page table, and when xv6 switches between processes, it also changes page tables." Hailperin §7.5.2: "the VMM does another level of mapping, translating the virtual machine's 'physical' page frames into the truly physical page frames of the hardware."

Demonstration: - bin/glint-run aarch64 --type guest_space prints "Guest space: 16 MiB at 0x40000000, host 0x4000a000, 4096 pages walked; 0x40123000 -> 0x4012d000". The host address is the base plus 0x123000. --no-virtualization, at EL1, prints the same line. - bin/glint-run x86_64 --type guest_space prints "Guest space: 16 MiB at 0x0, host 0x1a0000, 4096 pages walked; 0x123000 -> 0x2c3000", again the base plus 0x123000. - Typing it twice in one boot works: the first space is freed before the second is built. A hosted prompt answers "guest_space: native mode only (firmware owns the page tables)". - 3.4's boots are unchanged: the heap native and hosted, cat, fault "write" and overflow. - crystal spec, with QEMU_SRC, UBOOT_SRC, ZEPHYR_SRC, GLINT_UBOOT_BUILD_DIR, GLINT_QEMU_X86_64 and GLINT_QEMU_AARCH64 set, passes 699 examples with 0 failures, 0 errors and 0 pending, and leaves TMPDIR empty. spec/guest_space_spec.cr checks both formats against hand-encoded literals and the VTCR_EL2 value with its cap and RES1 bit. It checks translate at every edge, that only the space's own zeroed RAM is mapped, that free returns 3.1's free count to where it was, and that allocation and builder failures are statuses that lose no pages. - crystal tool format --check passes.

Size: 266 non-spec lines added and 1 removed, against ~330; spec +126. Largest function: the nested PageTable#map, 1,296 bytes; Shell.guest_space is 1,037. Images: BOOTAA64.EFI 164,864 -> 168,960 bytes; BOOTX64.EFI 164,352 -> 172,544.

Review: - The first run, 36c11892, stopped with the model at capacity and left an unusable patch, mostly cache bitcode inside the tree. It wasn't applied. This is run 29624d71, from 6076f190, and the patch's SHA3 matched the node's record. - The command is guest_space, not the phase text's guest-space. Codex had changed the shell lexer to read a hyphen inside an identifier. That breaks P's rule that "Everything a person types to Glint is Crystal syntax": Crystal parses guest-space as guest - space. The reviewer dropped the lexer change, renamed the command, and corrected docs/phases/03-page-tables.md and the task to match. - Codex was right that "3.2's format plus U/S" would have left guest RAM non-executable under 3.3b's NX. The nested format clears NX for guest RAM. - Only the spec checks VTCR_EL2's RES1 bit 31; no source here states it and QEMU doesn't check it. - The reviewer ran every boot and the full suite. - Second run. Verdict: merge. check-in: 86dd5dbc21 user: glint-session tags: trunk

01:51
Task 3.5: a guest address space (stage-2 MemAttr, S2AP, XN and VTCR_EL2 fields checked against QEMU 11.1.2's ptw.c and internals.h) check-in: 6076f190f2 user: glint-session tags: trunk
Changes
Unified Diff Side-by-Side Diff Patch
Changes to boot/efi_main.cr.
Changes to boot/mmu_aarch64.S.
Changes to docs/phases/03-page-tables.md.
Changes to docs/tasks/3.5.md.
Added mem/guest_space.cr.
Changes to mem/pte_aarch64.cr.
Changes to mem/pte_x86_64.cr.
Added spec/guest_space_spec.cr.
Changes to spec/native_table_spec.cr.
Changes to spec/shell_spec.cr.
Changes to user/shell.cr.