Login
Phase 3: Page tables
Login

xv6 §3, "Page tables". "Page tables determine what memory addresses mean, and what parts of physical memory can be accessed."

Phase 3 gives Glint control of memory: first its own, then a guest's. It starts where Phase 2 ended. Every boot now loads its files before the exit (2.9) and leaves boot services by default (2.10). At the exit it reads the final memory map into 2.3's buffer (2.6): the map read last, just before ExitBootServices, which describes the machine Glint now owns. It then moves onto a 64 KiB stack in its own image, with a spare page below it kept for this phase (2.6), and installs vectors that report any fault (2.7). Its native system table (2.5) already has AllocatePages and FreePages entries, stubs that answer EFI_UNSUPPORTED until this phase fills them. Phase 3 gives Glint a page allocator of its own (3.1) and a page-table builder (3.2). It moves Glint from the firmware's page tables onto its own (3.2a, 3.2b), uses them to catch stack overflows (3.3) and stray writes (3.3b), and adds a heap (3.4). It ends with a guest address space (3.5) and a guest image read from the preload (3.6) and placed in one (3.6b), ready for Phase 4 to enter.

Why the firmware's tables are in the way. This paragraph is the phase's one statement of it, and the slices point here. Until 3.2a and 3.2b, Glint runs on the page tables the firmware left, and they lie in memory the map calls usable. U-Boot's aarch64 tables are in the boot-services range add_u_boot_and_runtime marks (lib/efi_loader/efi_memory.c). On x86_64 the live tables are still the ones U-Boot's SPL built to enter 64-bit mode, at physical 0x80000 (PAGETABLE_BASE and cpu_jump_to_64bit_uboot in arch/x86/cpu/i386/cpu.c). They map only the first 4 GiB, and the q35 map lists their pages as EfiConventionalMemory. So no range from the map is safe to hand out, or even to write, until Glint's own tables are loaded.

Most of the phase needs native mode, because firmware owns the MMU until the exit. A boot that stays hosted, because it asked to or because 2.6's checks failed, runs only 3.4: the heap takes its pages through the system table's AllocatePages, and the firmware answers with EfiLoaderData pages. 3.1's allocator, Glint's tables, guard pages and guest address spaces do not run in hosted mode, and the Mode: line already says why the boot stayed hosted. A hosted boot that later types native keeps its heap: its pages are EfiLoaderData in the final map, and 3.2a maps every such range.

The builder's logic is shared between architectures; only the entry formats and the registers that load a table differ. Three slices split under rule 3, because each would pass ~400 lines whole. The builder (3.2) lands before Glint's tables are loaded with it, which splits along the architectures (3.2a, 3.2b) as rule 6 names them. Guard pages with their exception stacks (3.3) land before the narrower permissions (3.3b). The image parser (3.6) lands before placing an image at boot (3.6b). The numbers the threat model (2.8) cites keep their plain form: 3.1, 3.3, 3.5 and 3.6 are the slices it names, and its bullet on reusing firmware memory cites 3.2a and 3.2b. 3.3 stays one check-in for both architectures, though its exception stacks differ (a stack-pointer switch on Arm, a TSS on x86), because each is a few dozen lines.

The boot's lines keep Phase 2's fixed order. Before the exit nothing changes. After it, through Zephyr's UART: Left boot services, the final map's summary, 3.2a's (or 3.2b's) Page tables: line, 3.1's Pages: line, Mode: native, 3.4's Heap: line and, when the preload holds guest.efi, 3.6b's Guest space: and Guest image: lines. A hosted boot adds only 3.4's Heap: line, after its Mode: line, and prints it once: typing native later does not print it again. The overflow (3.3) and guest_space (3.5) commands print their lines when typed, and the shell's help lists both. The shell prompt comes last either way. A single bin/glint-run --expect shows that one line appeared; only the phase demo, spec/run/phase3_spec.cr, checks where each line falls.

Phase 2's lessons, recorded under Build constraints in the plan and in docs/TUTORIAL.md, bite throughout, and each slice says where. Image code runs without Crystal's start-up, so a constant or class variable whose value must be computed is zero in the image, and spec/image_initialization_spec.cr refuses it. Module and class state here is declared uninitialized and filled at call time, and register and descriptor values are literals or computed in methods. A StaticArray passed by value is copied by unrolled code: 2.9's first build grew BOOTX64.EFI from 119,296 to 279,040 bytes that way. Tables, range lists and image headers here are passed by pointer. On x86_64 every protocol function Glint provides or calls crosses the Microsoft calling convention, so each needs an ms_abi wrapper, in c/native_table.c or c/efi_boundary.c. And Crystal checks integer arithmetic: an overflow is a panic since 2.7c, so address arithmetic on outside data (map entries, image headers, guest addresses) is bounded before it is done, as MemoryMap.available does, and a hostile value is refused with a status instead of stopping Glint. Phase 2's slices came out at 1.2 to 2.6 times their estimates, largely for these reasons and for EFI protocol boilerplate. The sizes below are estimates after that factor.

The recorded maps in spec/fixtures/memory_map/ have no EfiLoaderData entry and no runtime EfiMemoryMappedIO entry, since they were recorded before the preload. Specs that need them synthesise them, adding entries to the parsed maps, and say which.

The slices below were refined when the phase started (rule 9). Every quoted passage was checked against xv6-riscv-book commit fa3b46bc43 and Hailperin's LaTeX source. Sizes are non-spec lines, as in rule 2.

Slices

3.1 Page-frame allocator. mem/pages.cr hands out and takes back 4 KiB pages of physical memory, the page frames every later slice is built from. It fills two entries of 2.5's native table, AllocatePages and FreePages, in place of their EFI_UNSUPPORTED stubs, so Glint's code asks the system table for pages in either mode, as principle 2 requires: the firmware answers in hosted mode, and this allocator in native mode. Its input is the final memory map, never 2.3's earlier copy. It may hand out 2.3's usable memory (EfiConventionalMemory, EfiBootServicesCode and EfiBootServicesData) and nothing else. It never hands out EfiLoaderCode (Glint's image), EfiLoaderData (2.9's preloaded files, and any pages the heap took from the firmware before a late native), runtime-services code or data, EfiACPIReclaimMemory or EfiACPIMemoryNVS (where U-Boot keeps the ACPI tables and its copy of the devicetree), or reserved and memory-mapped I/O ranges. It also never hands out physical page 0, so a null pointer never names a page in use. Because the firmware's live tables lie in usable memory (see Why the firmware's tables are in the way), the allocator withholds every range taken from the map until Glint's own tables are loaded and 3.2a (or 3.2b) calls Pages.release. Until then it hands out only a pool of 32 pages in Glint's own .bss (c/page_pool.c, page-aligned like 2.6's stack in c/native_stack.c), which is enough for Glint's tables and which no one else can be using. xv6 threads its free list through the free pages themselves. Glint's allocator keeps its free memory as a table of ranges in its own image instead, for two reasons: before Glint's tables are live it may not write into free memory, and a range table also serves requests for several contiguous pages and recognizes a double free exactly. The table holds 512 ranges, more than the 409 descriptors 2.3's buffer can hold, so seeding always fits. A free that would need a 513th range panics with pages: range table full; no slice in this phase frees pages scattered enough to reach it. It is seeded at the top of glint_native_continue (boot/efi_main.cr), after 2.6's stack switch and 2.7's vectors and before 3.2a's switch, from the map 2.6 read. 3.2a's switch runs before the native table exists, so it calls Pages.allocate directly; everything after the native table is built asks through the system table. AllocatePages takes AllocateAnyPages, carves the lowest range that fits and answers EFI_OUT_OF_RESOURCES when none does; other allocation types answer EFI_UNSUPPORTED until a slice needs them. Its MemoryType argument is checked, and a type UEFI forbids callers to allocate (EfiConventionalMemory, EfiPersistentMemory, an unaccepted or out-of-range value) answers EFI_INVALID_PARAMETER. Otherwise the type is not recorded, since after the exit no one reads a memory map again. FreePages answers EFI_INVALID_PARAMETER for an unaligned address. It answers EFI_NOT_FOUND, which UEFI gives for pages AllocatePages did not allocate, for pages already free or outside the allocator's domain. It fills each freed page with the byte 1, as xv6's kfree does, so code that uses a page after freeing it reads junk, and merges the range with its neighbours. After the final map's summary, a native boot prints Pages: N free, W withheld. Until Glint's tables are loaded, N is the pool's 32 and W the map's usable pages. W becomes 0 on aarch64 when 3.2a lands and on x86_64 when 3.2b lands. The range table is module data declared uninitialized, filled at call time and passed by pointer. On x86_64 both new entries get ms_abi wrappers in c/native_table.c, beside LocateProtocol's. In hosted mode nothing in this slice runs. spec/pages_spec.cr seeds the allocator from both recorded maps, with synthesised EfiLoaderData and runtime entries. It checks that no page handed out is of a forbidden type or page 0, and that only the pool is handed out before release. It checks exhaustion, double frees, unaligned frees, forbidden memory types and merging, and calls both entries through the native table. On firmware, bin/glint-run aarch64 --expect "Pages: 32 free" (and x86_64) shows the line. Its passages are xv6 §3.4 ("Physical memory allocation"), which says xv6 "allocates and frees whole 4096-byte pages at a time", and §3.5 ("Code: Physical memory allocator"), which admits what Glint does instead: "Xv6 ought to determine how much physical memory is available by parsing configuration information provided by the hardware." It opens the phase because every later slice that needs memory gets it here, Glint's own tables first. Answering through the same system-table entries in both modes, so that no caller knows which provider is behind them, is Loose Coupling. About 300 lines.

3.2 A page-table builder. mem/page_table.cr builds page tables, in host-testable Crystal (principle 3), and nothing in this slice loads one. Both architectures use the same tree, as xv6's Sv39 does with one level fewer: four levels of 512 eight-byte entries over 4 KiB pages, numbered as Arm numbers them, level 0 at the root to level 3 at the pages, with 48-bit addresses. A level-2 entry may instead map a whole aligned 2 MiB block. The builder is a generic struct, PageTable(F, P), whose type parameters are an entry format F and a page source P, so each kind of table compiles to its own code with no dynamic dispatch and no heap. A page source answers allocate : UInt64, the physical address of a zeroed page, or 0 when it has none: in the image it is 3.1's Pages, called directly, and in specs a fake over host memory. A format encodes and decodes entries: table(address), leaf(address, kind, level), valid?(entry), table?(entry, level) and address(entry). A kind names what a mapping is for, such as normal memory or device memory, and the format turns it into bits; 3.3b adds more kinds. This slice brings two formats: Arm's stage-1 descriptors (mem/pte_aarch64.cr, a MAIR index for the memory type, with a variant for each of EL2 and EL1) and x86's long-mode entries (mem/pte_x86_64.cr, present, writable and page-size bits). 3.5 adds Arm's stage-2 descriptors and reuses x86's for AMD's nested tables. The interface is two calls, as xv6's mappages and walk. map(va, pa, size, kind) : UInt64 installs a range, writing a level-2 block wherever the range covers an aligned 2 MiB and level-3 pages elsewhere, and returns an EFI status: 0; EFI_INVALID_PARAMETER for an unaligned or wrapping range, or one past 48 bits; EFI_OUT_OF_RESOURCES when the page source is empty; and EFI_ACCESS_DENIED when the range overlaps an existing mapping, which in Glint is always a layout bug. walk(va, alloc : Bool) : UInt64* returns the entry that maps va, a level-3 page or a level-2 block, creating missing tables when alloc is set, or a null pointer. The root is allocated when the table is made, and root : UInt64 gives its address. Table addresses are used as pointers, which is right in the image, where Glint's tables are an identity mapping (3.2a), and in specs, where the fake page source hands out host addresses. spec/page_table_spec.cr builds tables in both formats and compares them, entry by entry, with expected entries encoded by hand from the Arm ARM and the Intel SDM. It also checks blocks against pages at every alignment, the three errors, and a page source that runs out midway. At rung 2 both images link it. Its passage is xv6 §3.3 ("Code: Creating an address space"): "walk descends the page table tree one level at a time, using each level's 9 bits of virtual address to index into the relevant page directory page." Hailperin §6.3.3 ("Multilevel Page Tables") explains why a tree: such tables "locate the stored chunks without recursive use of virtual memory by using a tree data structure, rather than a single array." It comes after 3.1, whose Pages is the page source it is written for, and before 3.2a and 3.2b, which load what it builds. One builder for every table Glint makes, its own and later its guests' (3.5), is Parsimony in Tambassi's sense (one kind of mechanism before many, [40]). About 280 lines.

3.2a Glint's own tables on aarch64. Glint builds the tables it will run on with 3.2's builder and loads them, so that from here on what an address means is Glint's decision, not the firmware's. boot/kernel_map.cr decides what to map, from the final map, Glint's image and Z.8's device table, and is shared with 3.2b. Everything is mapped at its physical address, an identity mapping (xv6 calls it "direct mapping"). Glint was relocated to wherever the firmware loaded it and runs there. Every pointer it holds is physical: the image's, the stack's, 2.9's preload table, the system table's runtime-services and configuration-table pointers, and the device table's register addresses. U-Boot's tables map the same way. So the switch changes no address in use. The layout maps all usable memory, so that every page 3.1 hands out is reachable at its own address. It maps Glint's image, which holds its stack and 3.1's pool, and every EfiLoaderData range in the final map: the preload's, and any pages a hosted heap took before a late native. It maps runtime-services code and data, and any EfiMemoryMappedIO range the map marks EFI_MEMORY_RUNTIME, since the runtime services keep running at their physical addresses (Glint never calls SetVirtualAddressMap). It maps the ACPI and devicetree memory the configuration tables point into. Ranges of one kind that touch are merged first, so that blocks can be used across them. And it maps the registers of each device in Z.8's table, as device memory, so that Zephyr's PL011 driver keeps working with CONFIG_MMU unset, as Track Z states. Z.8's table records each device's base address but not its size, so each device gets the one 4 KiB page that holds its base. spec/kernel_map_spec.cr reads the build devicetree (compat/zephyr/dts/qemu-virt.dtb, through Cleave::Fdt) and fails if a device in the table has a reg larger than a page, so a bigger device cannot arrive half-mapped. Reserved memory, page 0 and everything else stay unmapped, so a stray access faults and 2.7's vectors report it. In this slice everything mapped as memory is readable, writable and executable; 3.3b narrows that. The switch, glint_mmu_switch in boot/mmu_aarch64.S, is called from the top of glint_native_continue, after 3.1 is seeded and the tables are built, and before the native table and Zephyr's console come up, so the console runs through Glint's device mapping from its first byte. At EL2 it first checks that HCR_EL2.E2H is clear, since the EL2 register layouts below assume it. It writes MAIR (index 0 for normal write-back memory, index 1 for Device-nGnRE), TCR and TTBR0, at EL2 or EL1 as 2.2 reported. TCR gets a 4 KiB granule, T0SZ 16 (48-bit addresses, the most a 4 KiB granule allows without FEAT_LPA2), and inner-shareable write-back table walks. Its output-address size copies ID_AA64MMFR0_EL1.PARange, which is safe even where it reports 52 bits, as QEMU's -cpu max does, because 52 acts as 48 with a 4 KiB granule. The two TCRs differ only in where that size goes (PS in bits 18:16 at EL2, IPS in bits 34:32 at EL1) and in TCR_EL2's RES1 bits 31 and 23; at EL1, EPD1 also turns off walks through TTBR1. The routine issues a dsb so the CPU's walker sees the finished tables. It turns translation off (SCTLR.M) with an isb, using only registers while translation is off, loads the three registers and invalidates the TLB (tlbi alle2 or tlbi vmalle1, then dsb and isb). Then it turns translation back on, with another isb, so that no entry cached from U-Boot's tables can conflict with Glint's. Before switching it saves the firmware's root, read from TTBR0, in KernelMap's module state, because the line that reports it prints only once the console is up. After the switch it calls 3.1's release, and once the console is up it prints Page tables: TTBR0_EL2 0x<firmware's root> -> 0x<Glint's root>. If building fails, Glint writes Page tables failed: 0x<status> through 2.6's poll_out path before any switch, and halts. The status is EFI_OUT_OF_RESOURCES (0x8000000000000009) when the pool runs out, or EFI_ACCESS_DENIED for an overlap. spec/kernel_map_spec.cr builds the layout from both recorded maps, with synthesised EfiLoaderData and runtime-MMIO entries, a fake image and Z.8's device table. It walks every class of address: image, stack, pool, loader data, runtime services, configuration tables, the UART as device memory, and page 0 and reserved memory unmapped. It also checks that the tables fit in the pool with room to spare. On firmware, bin/glint-run aarch64 --type 'cat "hello.txt"' --expect "Hello from the ESP!" reads a preloaded file through Glint's tables, and its log shows Page tables: TTBR0_EL2. With --no-virtualization the line names TTBR0_EL1. Until 3.2b lands, x86_64 boots stay on U-Boot's tables and 3.1's pool. Its passages are xv6 §3.2 ("Kernel address space"): "The kernel maps all physical RAM and device registers at virtual addresses equal to the physical addresses." And §3.3, on the moment of the switch: "The kernel continues to execute correctly because the kernel page table is direct-mapped, so that addresses refer to the same locations in RAM before and after this change." It comes after 3.2, whose builder it uses, and before 3.2b because aarch64 leads (rule 6). It is where Glint stops depending on the firmware's mappings. Mapping everything at the address Glint already holds for it, so that no pointer changes meaning, is Clarity. About 330 lines.

3.2b Glint's own tables on x86_64. The same as 3.2a on x86_64: 3.2's x86 format, 3.2a's layout, and glint_mmu_switch in boot/mmu_x86_64.S, which loads the root into CR3 from the same place in glint_native_continue. Paging cannot be turned off in long mode, so the switch is a single write. It also drops every TLB entry not marked global, and U-Boot's are not (build_pagetable in arch/x86/cpu/i386/cpu.c sets no global bit), so nothing else needs invalidating. The x86 build class has no memory-mapped device yet. Its only device, the NS16550, is reached through I/O ports (io-mapped in compat/zephyr/dts/pc-com1.dts), which page tables do not translate, and its reg of 0x3f8 is a port number, not an address. Z.8's table does not record io-mapped; 6.8 adds the flag. Until then the layout maps no device on x86_64, and spec/kernel_map_spec.cr fails if the x86 table holds any device other than the NS16550, so a memory-mapped device cannot arrive unmapped and unnoticed. As on Arm, the slice saves the firmware's root, calls 3.1's release, and prints Page tables: CR3 0x80000 -> 0x<Glint's root>, which also shows the firmware tables 3.1 had to avoid. spec/kernel_map_spec.cr runs the recorded q35 map through the x86 format. On firmware, bin/glint-run x86_64 --type 'cat "hello.txt"' --expect "Hello from the ESP!" reads a preloaded file through Glint's tables, and its log shows Page tables: CR3 0x80000. Its passage is xv6 §3.1 ("Paging hardware"): "To tell a CPU to use a page table, the kernel must write the physical address of the root page-table page into the satp register." CR3 is x86's satp, and Hailperin §6.3.3 describes it in the same words: "The operating system on an IA-32 machine stores the physical base address of the page directory in a special register, where the hardware's page table walker can find it." It follows 3.2a because aarch64 leads (rule 6). Only the switch differs from 3.2a, so nothing above it knows which CPU it maps for, which is Loose Coupling. About 100 lines.

3.3 Guard pages and exception stacks. With Glint's own tables live, the layout leaves the page below each of Glint's stacks unmapped, a guard page, and each architecture gets a stack to report the resulting fault on. c/native_stack.c holds them all: 2.6's stack, whose lowest page 2.6 kept spare for this, and a new exception stack of 16 KiB with an unused page below it. Both lowest pages become guards. A guard alone is not enough, because on both architectures the CPU starts reporting a fault on the stack that has just overflowed. On aarch64 the vector's sub sp, sp, #256 does not fault, but the stp that follows it does (boot/vectors_aarch64.S). Each nested fault lowers SP by another 256 bytes, so after about 16 of them SP has left the 4 KiB guard. The stores then land in the image's .bss below the guard, which is silent corruption. So from the exit on, Glint runs on SP_EL0, and an exception, which always switches to SP_ELx, lands on the exception stack. The stack switch 2.6 wrote, glint_switch_native_stack in boot/crt0.S, now sets SP (still SP_ELx) to the exception stack's top, sets SPSel to 0, and sets SP, which is now SP_EL0, to 2.6's stack, before it installs the vectors. The report prints the interrupted SP_EL0. Phase 4's run loop saves Glint's SP_EL0 with the guest's state, since a guest's EL0 uses the same register. On x86_64 a page fault on the overflowed stack cannot push its frame, so it becomes a double fault (vector 8). 2.7b's gates all use IST 0, the current stack, so the double fault cannot be delivered either, and the CPU shuts down: QEMU resets with nothing printed, as the comment in boot/vectors_x86_64.cr warns. So this slice gives x86 a 64-bit TSS, whose descriptor takes two more GDT entries and is loaded with ltr. Its IST1 points at the exception stack, and only vector 8's gate uses IST1, as Linux does. The report prints CR2 for a double fault as well as for a page fault, and does not rely on the saved RIP, which the Intel SDM leaves undefined for vector 8. The GDT and TSS are filled at call time, in install, as 2.7b fills its GDT. On both architectures, when the faulting address (FAR, or CR2) lies in a guard page, the report adds Stack overflow: guard page at 0x<address>. The shell's new overflow command first prints the range of the guard below its stack, overflow: guard page 0x<start>-0x<end>. It then recurses, with a frame the compiler cannot turn into a loop, until it hits the guard. In hosted mode it refuses, as fault does, because the firmware owns the stack and the tables. spec/kernel_map_spec.cr checks that both guard pages are unmapped in both formats. spec/panic_vectors_spec.cr checks the overflow line and the CR2 line for vector 8 from given register values, and the TSS, GDT and gate encodings. On firmware, bin/glint-run aarch64 --type overflow --expect "Stack overflow: guard page" shows the line, after Panic: data abort. On x86_64 the report's first line is Panic: double fault, and the overflow line follows it. The phase demo checks that the address lies in the range overflow printed. Its passage is xv6 §3.2: "The guard page's PTE is invalid (i.e., PTE_V is not set), so that if the kernel overflows a kernel stack, it will likely cause a page fault and the kernel will panic." xv6 maps its kernel stacks high, so that a guard costs no physical page, and notes that with only a direct map "providing guard pages would involve unmapping virtual addresses that would otherwise refer to physical memory, which would then be hard to use." Glint keeps the direct map and gives up one page per stack, which for two stacks is cheap. It comes after 3.2a and 3.2b because only Glint's own tables can leave a page unmapped. Turning silent corruption, or a silent reset, into a report at the right address is Demonstrability. About 340 lines.

3.3b Permissions. The layout stops mapping everything as readable, writable and executable, so that a stray write or jump faults too. boot/efi.lds puts the PE header, .text with its read-only data, .dynamic, .rela.dyn and the dynamic symbol tables below _etext, and those pages become read-only and executable. .reloc, from _etext to _data, becomes read-only and never executable. .data and .bss become writable and never executable. The preload's ranges, found through 2.9a's table, and the configuration tables become read-only and never executable. Other EfiLoaderData, such as a hosted heap's pages, and usable memory become writable and never executable. Runtime-services code stays executable and its data writable. Device memory is never executable. On Arm, AP[2] makes a page read-only. Execute-never depends on the level: at EL2, with HCR_EL2.E2H clear, there is one XN bit (54) and AP[1] is RES1; at EL1 there are PXN (53) and UXN (54), and only PXN stops EL1 executing, so the EL1 format sets both. On x86 the NX bit (63) is honoured only once EFER.NXE is set, and ring 0 obeys read-only pages only once CR0.WP is set; glint_mmu_switch sets both before loading CR3. 3.2's formats gain the new kinds. spec/kernel_map_spec.cr checks each kind's bits in all three formats (Arm at EL2, Arm at EL1, x86) and every class of address in both recorded maps. The shell's fault command gains fault "write", which prints the address of an instruction in .text and then stores to it. On firmware, bin/glint-run aarch64 --type 'fault "write"' --expect "Panic: data abort" (and x86_64, "Panic: page fault") shows the store refused, and the phase demo checks that FAR (or CR2) is the printed address. With --no-virtualization the same runs at EL1. Its passage is xv6 §3.2: "The purpose of these restricted permissions is to help catch kernel bugs that access pages in unexpected ways, for example if kernel code accidentally tried to write over kernel instructions." It comes after 3.3, which leaves holes in the layout, and before the heap and guests, so that every later slice runs with its stray writes caught. Stating each kind of memory's permissions once, in the layout, is Clarity. About 150 lines.

3.4 Kernel heap. mem/heap.cr gives image code allocation of small objects, which the image has lacked. Until now every buffer has been a fixed array in .bss, and no Crystal class could be instantiated in the image. Crystal compiles new into a call to __crystal_malloc64 when the program defines one, and otherwise into a call to C's malloc; Glint's image has neither. The heap defines __crystal_malloc64, __crystal_malloc_atomic64 and __crystal_realloc64, and Glint::Heap.free. Every block starts with a 16-byte header recording its size class or page count, so free needs no size and every payload is 16-byte aligned. The header counts inside the class. Size classes are powers of two from 32 to 2048 bytes, each holding 16 bytes less than its size, so the largest class holds 2032 bytes and a request for 2 KiB takes whole pages. Each class keeps a free list threaded through its free blocks, as xv6's allocator threads its pages, which is safe here because all of the heap's memory is Glint's. A class whose list is empty takes one page and cuts it into blocks. A request above 2032 bytes takes whole pages, enough for the request and the header, so its payload sits 16 bytes into its first page: 16-byte aligned, not page aligned. Code that needs whole aligned pages calls AllocatePages itself. Memory comes back zeroed, as Crystal's own collector returns it. The heap takes its pages through the system table's AllocatePages, by EFI::Call.pages. So in hosted mode the firmware backs it with EfiLoaderData pages, which 3.2a maps if the boot later goes native, and the heap works the same (principle 2). It never gives pages back, so it never calls FreePages. Crystal frees nothing itself without a collector, so a class instance lives as long as Glint does unless Glint's code frees it, and the Boehm collector stays the isolated option principle 4 places after Phase 8. When AllocatePages fails, the heap panics with heap: out of memory rather than return a null pointer that Crystal code would not check. Its state, the class lists and the page count, is module data declared uninitialized and set on first use, with class sizes computed by shifts at call time, never held in computed constants. Before the first prompt, once per boot, a self-check runs in either mode. It allocates one block of each class and one of three pages, and checks that each is 16-byte aligned, zeroed and distinct. It frees one block and checks that the next allocation of that class returns it, and that __crystal_realloc64 keeps contents. Then it prints Heap: ready (N KiB) after the Mode: line, N being the KiB of pages the heap holds after the check. spec/heap_spec.cr runs the heap over the fake table's AllocatePages and checks the classes, the 2032-byte boundary, reuse after free, realloc, and the panic when pages run out. At rung 2, llvm-nm shows __crystal_malloc64 defined in both images. On firmware, bin/glint-run aarch64 --expect "Heap: ready" and the same with --mode hosted (and each for x86_64) show one heap over both providers. Its passage is xv6 §3.8 ("Real world"): "The xv6 kernel's lack of a malloc-like allocator that can provide memory for small objects prevents the kernel from using sophisticated data structures that would require dynamic allocation." In native mode it carves pages that must already be mapped, so it could land any time after 3.2b. It sits here, just before its first user, 3.5's guest address space. Keeping it apart from 3.1, so that each can be read and tested alone within the slice size, is Parsimony. About 240 lines.

3.5 A guest address space. mem/guest_space.cr builds a guest's address space: second-stage tables that map the addresses a guest believes are physical (guest-physical addresses) onto pages from 3.1. Phase 4 loads them when it enters a guest. On Arm they are stage-2 tables, named by VTTBR_EL2 and shaped by VTCR_EL2; on x86 they are AMD's nested page tables, named by the nested CR3 in the VMCB. 3.2's builder makes them. Arm's stage-2 descriptors differ from Glint's own in their attribute and permission fields (MemAttr and S2AP, in place of a MAIR index and AP), so mem/pte_aarch64.cr gains a stage-2 format. AMD's nested tables use the ordinary long-mode format, with every entry marked user-accessible because the CPU checks nested walks as user accesses, so x86 reuses 3.2's format with that one bit. A GuestSpace is a Crystal class, the heap's first user (3.4). It holds the guest's RAM, its root, and the register values Phase 4 will load. On Arm those are VTTBR_EL2, with VMID 0, and VTCR_EL2: a 4 KiB granule, T0SZ 16 for 48-bit guest-physical addresses, SL0 for a walk starting at level 0 to match, and PS copied from ID_AA64MMFR0_EL1.PARange, capped at 48 bits as in 3.2a. On x86 it is the nested CR3. Its register values are computed in methods and its fields set in initialize, never from computed constants. Guest RAM starts at 0x40000000 on Arm and at 0 on x86, where QEMU's virt and q35 machines put it, so a guest built for those machines finds RAM where it expects. RAM is taken in one AllocatePages call and zeroed before it is mapped, so no guest sees what Glint or another guest left there. Nothing else is mapped. Device ranges stay empty, so a guest's access to them traps to Glint, as Phase 5 needs and as the threat model states for pointers outside guest memory and for device registers. Here guest RAM is mapped whole; 5.7 later backs it only on first touch. translate(gpa, length, host : UInt64*) : UInt64 refuses (returns 0) a range that wraps or leaves guest RAM. Otherwise it walks the tables for gpa, stores the host address, and returns how many bytes from there are contiguous on the host, never past the end of that 4 KiB page. A caller copies page by page, as xv6's copyin and copyout do through walkaddr, and never assumes guest RAM is one host run, which 5.7 will break. 3.6b loads through it, and 4.5 checks guest arguments with it. Until Phase 4 has guests to run, the shell's new guest_space command builds one 16 MiB space and walks it back entry by entry with the same builder that made it. Then it translates the fixed guest address 0x40123000 (0x123000 on x86_64), prints Guest space: 16 MiB at 0x40000000, host 0x<RAM base>, 4096 pages walked; 0x40123000 -> 0x<host>, and frees the space, so 3.1's FreePages runs too. That walk shows only that the code runs and agrees with itself. Correctness rests on the spec, whose expected entries are encoded by hand. The translated address makes a wrong offset visible on firmware, since it must equal the host base plus 0x123000, which the phase demo checks. In hosted mode the command refuses, as fault does. spec/guest_space_spec.cr compares both formats with hand-encoded entries and checks the register values. It checks translate at every edge: ranges that wrap, ranges that cross the end of RAM, and a page boundary inside a range. And it checks that no page of Glint's own is ever mapped into a guest. On firmware, bin/glint-run aarch64 --type guest_space --expect "Guest space: 16 MiB" (and x86_64) shows it, and with --no-virtualization the space is still built and walked. Its passage is xv6 §3.6 ("Process address space"): "Each process has its own page table, and when xv6 switches between processes, it also changes page tables." Hailperin §7.5.2 ("Protection of Entire Simulated Machines") states the guest's case: "the VMM does another level of mapping, translating the virtual machine's 'physical' page frames into the truly physical page frames of the hardware." Hailperin goes on to have the VMM compose the guest's tables with its own in software, which is shadow paging. Glint leaves that composition to the hardware's second stage, and never builds shadow tables. It comes after 3.4, whose heap holds the GuestSpace. It reuses 3.2's builder rather than adding a second one, so there is one page-table mechanism in Glint, which is Parsimony in Tambassi's sense [40]. About 330 lines.

3.6 Reading a guest image. boot/pe_image.cr parses and checks a guest image, without placing it. The format is PE32+, the one UEFI loads. Glint's own images are PE32+, and so are the kernels What Linux sees boots through their EFI stubs, the arm64 Image and the x86 bzImage. So one parser serves every guest Glint will load, from Phase 4's test guest (4.2), built the way Glint's images are, to Linux (6.7a, 6.7b), and 6.5's guest firmware loads through it. A guest image is outside data (the threat model's ESP files), so the parser trusts nothing in it. It checks the DOS and PE signatures, the PE32+ magic and the EFI-application subsystem, and that the machine (0xaa64 or 0x8664) matches Glint's own. It checks that SizeOfImage fits in the space it is meant for from the load address, that every section's address and size lie inside SizeOfImage and its file data inside the file, and that the entry point lies in an executable section. It checks that the base-relocation directory lies inside the file and holds only well-formed blocks of DIR64 and padding entries. Every sum is checked for overflow before it is used, as xv6's exec checks ph.vaddr + ph.memsz, so a hostile size is refused with a status rather than reaching 2.7c's overflow panic. The parser reads the image in place, through a pointer and a length, and never copies its header into a StaticArray passed by value. Glint's own images are poor samples for relocation. Their PE .reloc holds one block of padding entries only (boot/crt0.S), because they relocate themselves through ELF RELA records at entry (c/efi_reloc.c). So this slice adds a test guest: tools/make_test_guest.cr writes spec/fixtures/guest/reloc_aarch64.efi and reloc_x86_64.efi. Each is a small PE32+ for its machine with a preferred base of 0x10000000. It has a code section whose entry is a branch to itself, a data section holding eight absolute addresses of places in the image, and a .reloc block with a DIR64 entry for each and padding. spec/test_guest_spec.cr checks that the fixtures are exactly what the tool writes now, so they cannot drift from it. spec/pe_image_spec.cr parses both fixtures and both built Glint images, and hand-made hostile headers: a wrong machine, a section beyond SizeOfImage, sizes that wrap, file data past the end, an entry outside the code, a relocation block past the directory, and an unknown relocation type. Its demonstration is at rung 1, with the built images read at rung 2; 3.6b takes it to firmware. This is the analogue of xv6 §3.7 ("Code: exec"), whose warning is the slice's reason: "Thus exec is risky, because the addresses in the ELF file may refer to the kernel, accidentally or on purpose." It comes after 3.5 and before 3.6b, which places what it accepts. Checking every header field against a written boundary, with specs that show the hostile cases refused, is Demonstrability. About 320 lines.

3.6b Placing a guest image at boot. When the preload holds guest.efi, a native boot builds a guest space with 3.5's code and places the image in it, and the space is kept for Phase 4 to enter. glint-run gains --guest PATH, which writes PATH to the ESP as guest.efi. The image is read in place: the boot finds guest.efi in 2.9a's preload table and hands 3.6's parser that entry's address and size. It does not open it through the SIMPLE_FILE_SYSTEM 2.9b serves, which would copy it. The space is 16 MiB, as guest_space builds, and an image whose SizeOfImage does not fit 2 MiB in is refused with the parser's status. The boot does not walk the space back; that check belongs to 3.5's command and spec. GuestSpace#load copies each section to the load address, 2 MiB into guest RAM, through 3.5's translate, page by page. It zero-fills the rest of each section, as xv6 fills the gap between filesz and memsz, and applies the image's DIR64 relocations for the difference between the load address and the preferred base. Then the boot prints Guest space: 16 MiB at 0x40000000, host 0x<RAM base>, followed by Guest image: guest.efi, N KiB at 0x40200000, entry 0x<address>, R relocations, crc32 0x<sum>. The sum is UEFI's CRC32, as NativeTable.crc32 computes it, over the SizeOfImage bytes as placed. A refused image prints Guest image: guest.efi refused: 0x<status>, and the boot goes on without a guest. Without guest.efi a boot builds no space. spec/pe_image_spec.cr places each fixture in a space over the fake table and checks it against the same placement computed on the host. On firmware, bin/glint-run aarch64 --guest spec/fixtures/guest/reloc_aarch64.efi --expect "8 relocations" (and x86_64 with its fixture) shows the line, and the phase demo compares the printed CRC with one computed on the host from the fixture at the same load address. Its passage is xv6 §3.7: "A program section header's filesz may be less than the memsz, indicating that the gap between them should be filled with zeroes (for C global variables) rather than read from the file." Like xv6's loadseg, which "loads into the process's page table, not in the kernel's page table", Glint writes the image only through the guest's own space, so no address in the image can reach Glint's memory. It comes last because it needs 3.1's pages, 3.5's address space, 3.6's parser and 2.9a's preload. A checksum computed independently on the host, rather than a line the boot prints about itself, is Demonstrability. About 200 lines.

Phase demo: on both architectures under QEMU and U-Boot, a default native boot runs on Glint's own page tables with every Phase 2 path still working. It hands out memory from the final map only once those tables are live. It reports a deliberate stack overflow at its guard page and a store into its own code, and places a relocated guest image whose checksum matches one computed on the host. Asked to stay hosted, its heap runs on the firmware's pages, and survives a later native.

The demo is spec/run/phase3_spec.cr, which needs QEMU_SRC, UBOOT_SRC and ZEPHYR_SRC. It is the only place that checks the order of lines, against the order stated at the top of this document. For each architecture it makes four runs. The first, bin/glint-run aarch64 --guest spec/fixtures/guest/reloc_aarch64.efi --type guest_space --type 'cat "hello.txt"' --type overflow --expect "Stack overflow: guard page", checks Phase 2's lines up to Left boot services and the final map's summary. Then it checks Page tables: TTBR0_EL2 (on x86_64, Page tables: CR3 0x80000), Pages: with 0 withheld, Mode: native and Heap: ready. Then come Guest space: and Guest image: guest.efi with 8 relocations and a CRC equal to the host's. Then come guest_space's line, whose translated address equals its host base plus 0x123000, and the file's contents. Last comes the overflow report (on x86_64 after Panic: double fault), whose address lies in the range overflow printed. The second, --type 'fault "write"' --expect "Panic:", checks that the faulting address is the one fault printed. The third, --mode hosted --type native --expect "Mode: native", checks Heap: ready once, after Mode: hosted (requested), and the native lines after the typed native, with no second Heap: line. The fourth, --no-virtualization --type guest_space --expect "Guest space:", checks that Page tables: TTBR0_EL1 follows Entered at EL1 (on x86_64, that the boot runs the same with SVM not available).

References