Memory Management

Memory management gives the kernel controlled ownership of physical frames, separates user processes, enforces page permissions, and exposes memory authority only through explicit capabilities.

Related

• Go VirtualMemory Contract records the reserve/commit/decommit contract that extended the VirtualMemory implementation for Go-style arena allocation.
• Userspace Runtime describes the typed VirtualMemoryClient surface used by allocator and runtime code.
• OOM Handling and Swap and Resource Accounting and Quotas define future memory-pressure and quota policy.
• Resource Governance defines structural versus policy limits, aggregate ownership, and exact reservation/release rules.
• Memory Authority Model defines the future cross-cutting contract for memory authority classes, residency, mapping consistency, pins, DMA boundaries, swap eligibility, and proof obligations.

Current Behavior

The frame allocator builds a bitmap from the Limine memory map, marks all non-usable frames as used, reserves frame zero, and reserves its own bitmap frames. The heap is initialized separately for kernel allocation.

Paging initialization builds a new kernel PML4, remaps kernel sections with section-specific permissions, copies upper-half mappings with NX applied and user access stripped, switches CR3, then enables page-global support. SMEP/SMAP are enabled after those mappings are active.

Each user AddressSpace owns its lower-half page tables and clones the kernel’s upper-half mappings. Dropping an address space walks the user half and frees mapped frames, committed anonymous frames retained behind VM_PROT_NONE, and page-table frames. VirtualMemory lets a process reserve anonymous address ranges, commit and decommit physical backing, unmap reservations, and protect committed pages. Anonymous reservations charge the process virtual reservation ledger. Committed anonymous pages charge ResourceLedger::frame_grant_pages.

FrameAllocator allocation methods return a MemoryObject result capability, not a physical address. The normal result payload carries the result-cap index, and the CQE transfer-result record carries the local cap id plus MemoryObject interface id. MemoryObject.info exposes page count and size; MemoryObject.map maps page-aligned object ranges into the caller address space, MemoryObject.unmap removes those borrowed mappings, and MemoryObject.protect updates their page-table flags. Held MemoryObject caps charge the holder’s frame_grant_pages ledger, and final CAP_OP_RELEASE or process exit frees the owned frames once no borrowed address-space mapping still holds the backing alive.

The enforced frame-grant and virtual-reservation maxima currently come from the process ledger/ABI construction path, not from the manifest memoryCommitLimitBytes or frameGrantLimitPages profile fields. Those fields remain policy data until profile binding reaches the memory owner and defines how byte commitment and page grants compose. Current release helpers also use defensive saturating/no-op behavior in places; the accepted target is a typed generation-bound reservation whose duplicate, oversized, stale, or missing release is detected rather than silently absorbed.

Design

The kernel keeps physical allocation host-testable by placing bitmap logic in capos-lib and wrapping it with kernel HHDM access in kernel/src/mem/frame.rs. Page-table manipulation stays in the kernel because it is architecture-specific.

ELF loading and VirtualMemory both use page-table flags to preserve W^X: non-executable data gets NX, writable mappings are explicit, and userspace pages must be USER_ACCESSIBLE. The CapSet and ring bootstrap pages occupy reserved virtual pages; VirtualMemory rejects ranges that overlap either one.

User-buffer validation for published processes uses the process AddressSpace mutex. The kernel checks that user pointers stay below the user address limit, verifies page-table permissions for the requested read/write access, and copies through the HHDM mapping while holding the same address-space lock. This keeps validation and use tied to one stable page-table view. The shared mem::validate::user_buffer_bounds helper checks arithmetic and user-range bounds only; there is no separate current-CR3 page-table validator. Spawn-time TLS initialization uses the same copy primitive while the new address space is still exclusively owned and has not been published to the scheduler.

Committed VirtualMemory pages and held MemoryObject caps use the same per-process frame-grant ledger, with quota checks before frame allocation or mapping side effects. Anonymous reservation consumes a separate virtual page quota, so guard ranges and Go-style sysReserve arenas do not spend physical commit budget. Held MemoryObject caps charge for the backing they keep reachable, and each live borrowed MemoryObject mapping reserves frame-grant pages until it is unmapped. This prevents a process from mapping an object, releasing the cap to drop the cap-slot charge, and keeping the backing pinned without quota. The address space records borrowed pages separately from sparse anonymous reservations so teardown and unmap can distinguish anonymous pages from object-backed pages. Future file/network/DMA resources should reuse that authority ledger instead of adding one-off counters per cap.

Invariants

• Frame addresses are 4 KiB aligned.
• The frame bitmap’s own frames are never returned as free frames.
• Upper-half kernel mappings are not user-accessible.
• Kernel text is RX, rodata is read-only NX, and data/bss are RW NX.
• User address spaces own only lower-half page-table frames.
• Process frame-grant usage covers committed anonymous VM pages, held MemoryObject caps, and live borrowed MemoryObject mappings.
• Process virtual-reservation usage covers reserved anonymous VM pages whether or not they are committed.
• Committed VM_PROT_NONE pages retain their frames and data while exposing no present user PTE; reserved uncommitted pages consume no frame-grant quota.
• Object-backed user mappings are tracked as borrowed pages and hold the MemoryObject backing alive until unmapped or address-space teardown.
• MemoryObject unmap/protect only succeeds for borrowed pages backed by the same object.
• VirtualMemory caps are bound to one address space and are not valid cross-process service exports.
• CapSet is read-only/no-execute; ring is writable/no-execute.
• VirtualMemory cannot reserve, map, commit, decommit, unmap, or protect the ring or CapSet pages.
• VirtualMemory commit/decommit/protect/unmap only succeeds for ranges covered by anonymous reservations owned by the cap’s address space.
• Capability-ring CALL/RECV/RETURN buffers, transfer descriptors, process and thread wait completions, and private ParkSpace word reads must validate and copy/read while holding the target process AddressSpace lock.

OOM Boundary Normalization

The untrusted-reachable memory-authority capabilities distinguish four typed allocation-failure classes. Every class is a transient “temporary lack of resources” condition in the Cap’n Proto sense – releasing capabilities/reservations/frames or retrying later can succeed – so all four serialize as overloaded (never failed). They are told apart by a stable, machine-greppable token appended in brackets to the exception message. capos_lib::mem_failure (MemoryExhaustion) is the single source of truth for the class-to-token mapping; the kernel constructs the error through cap::memory_exhaustion_error, which routes it to overloaded and appends the token.

Before this normalization the same failure produced different wire types across files: the per-process frame-grant quota was failed in kernel/src/cap/virtual_memory.rs but overloaded in kernel/src/cap/frame_alloc.rs, and real physical OOM was failed while cap-table publication OOM was overloaded. The classifier removes that split, including the page-table-frame OOM inside map_to: the first-mapping paths (VirtualMemory.commit, MemoryObject.map, and VirtualMemory.protect transitioning a VM_PROT_NONE-committed page to an accessible protection – which is that page’s first map_to, since a VM_PROT_NONE commit never maps) route MapToError::FrameAllocationFailed to global-frame-pressure rather than collapsing it to failed. The protect-rollback re-map path re-maps an address whose intermediate page tables already exist, so map_to cannot allocate a new page-table frame there; it keeps the plain failed string for its genuine internal-invariant faults.

Kernel-internal bookkeeping allocations (TLB deferred-completion slots, reservation/commit tracking Vec growth) are not one of these four caller-attributable classes; they already fail closed as generic overloaded and are intentionally untokened.

ProcessSpawner types image-load failures before the capability boundary. Physical-frame exhaustion while creating the address-space root, mapping the ELF, stack, or TLS, or allocating an intermediate page table routes through GlobalFramePressure. Fallible kernel bookkeeping allocation during image construction remains an ordinary, untokened construction overload. Validation, address arithmetic, mapping, and copy invariant failures remain failed; they are not mislabeled as retryable memory pressure. Process/thread limits, child-cap construction, and scheduler run-queue capacity remain their existing distinct resource family and continue to report untokened overloaded results.

The DDF hardware-mapping paths (kernel/src/cap/device_mmio.rs, kernel/src/cap/dma_buffer.rs) also allocate page-table frames through AddressSpace::map, but those caps are privileged hardware authority granted only to trusted driver processes, not reachable by an untrusted process, so they are outside this untrusted-reachable taxonomy and keep their existing failed mapping errors.

Current State-Transition Inventory

This inventory describes the current implementation, not the future pin, swap, or shared-park design. A deferred TLB completion is part of a transition: frame reuse is not complete until the recorded remote shootdown generation has been acknowledged.

Authority, ledgers, and locks

Anonymous VirtualMemory

MemoryObject

Page-table and TLB completion paths

User-buffer stability paths

ParkSpace cleanup at memory transitions

The inventory records control flow; it is not a substitute for the remaining proofs. The failure-atomicity residual is now implemented – the post-mutation sections are infallible-after-preflight or restore a coherent state through an infallible rollback (see Transition Failure Atomicity). Exact remaining work is tracked by final MemoryObject release ordering, VM ownership host-test residuals, and the SMP TLB/frame-reuse proof. The accepted Shared Mapping Identity and Object Pins contract now defines the object identity, offset, generation, pin, and validation rules. Shared park keys remain disabled until those records, pins, and cleanup paths are implemented and proven.

Transition Failure Atomicity

Once a user-memory transition begins mutating page tables it must not return to userspace with page tables, ownership records, quota ledgers, or deferred-completion records disagreeing. Each untrusted-reachable transition (anonymous decommit/unmap/protect, MemoryObject.unmap/protect) is split into a fallible preflight that mutates nothing and an infallible commit:

• The preflight validates the range, resolves the tracking records, reserves the deferred-completion slots, and reserves any bookkeeping growth. Every failure that can be reached under quota or global pressure is raised here, before any page table or record changes, so a rejection leaves the exact before-state.
• The commit removes or re-flags leaf PTEs through the infallible primitives AddressSpace::unmap_present, AddressSpace::protect_present, and (for rollback re-maps) AddressSpace::remap_present. Each was proven present (or, for a re-map, proven to still own its intermediate tables) under the held address-space lock, so the underlying Mapper call cannot fail: unmap clears only the leaf entry and leaves L2/L3/L4 intact (so it never frees a frame the metadata still references), update_flags rewrites an existing leaf, and the rollback map_to reuses the intermediate tables unmap left behind and allocates nothing. A failure at that point means the hardware page tables have diverged from the tracking metadata under the lock – an unrecoverable invariant break – so the primitive fail-stops rather than hand userspace a partially torn-down range.

protect keeps one genuinely fallible commit step: a VM_PROT_NONE -> accessible transition performs the page’s first map_to, which can hit page-table-frame global-frame-pressure. On that failure the applied steps roll back newest first, and because every rollback sub-operation is one of the infallible primitives above, the rollback itself cannot fail: the range always returns to one coherent before-state instead of “returning from a failed rollback”.

Any frame a transition releases is handed to defer_frame_free, which holds it out of the allocator until the local flush and the remote shootdown completion for its page have finished (kernel/src/arch/x86_64/tlb.rs, drain_deferred_completions); borrowed MemoryObject frames are owned by the object backing and are freed on its Drop, so their unmap defers only the shootdown completion. VirtualMemory.decommit, VirtualMemory.unmap, and the commit rollback of already-committed pages all funnel their per-page unmap completion into defer_frame_free, whose drain_deferred_completions FreeFrame arm flushes locally, waits for the remote acknowledgement, and only then returns the frame. The ordering is structural – the wait() lexically precedes the free – and a cfg(qemu) tripwire in that arm prints an ORDERING VIOLATION line if a future edit ever removes or weakens that wait() so a frame reaches the allocator without its remote acknowledgement complete. make run-tlb-frame-reuse-ordering is the focused SMP proof that drives a real resident-sibling unmap through that exact machinery and shows same-physical reuse only after the ack. The immediate ring drain (cap_enter, service_sqpoll_snapshot) runs drain_deferred_completions before its deferred capability drops, so a same-drain final unmap and final release trigger that Drop only after every remote acknowledgement – frames are never returned to the allocator while a sibling may still hold a stale translation. A cfg(qemu) guard in MemoryObjectBacking::drop asserts no completion is pending at free, and make run-memoryobject-final-release-ordering is the focused SMP proof.

Two frame-free paths deliberately do not issue a shootdown, because no sibling CPU can hold a stale translation to the frame:

• Commit rollback of the just-allocated, never-mapped frame. When map_committed_page fails, the frame allocated for that page was never installed into a live PTE, so VirtualMemoryCap::commit_region frees it directly (kernel/src/cap/virtual_memory.rs). A frame that was never mapped cannot be cached in any TLB.
• Process exit (AddressSpace::drop). External termination removes a process only after it is nonresident (terminate_process_locked rejects a pid that is current or in handoff on any non-idle CPU; kernel/src/sched.rs), and a CPU that leaves a user address space reloads CR3 – to a successor or, on exit, the kernel PML4 (exit_current) – which in the current no-PCID scheduler evicts that space’s non-global user translations (user PTEs are never GLOBAL). Process removal / non-residency is therefore what makes a separate teardown shootdown unnecessary (see the “Live address space targeted externally” and “Borrowed mapping in a dying address space” rows above): the Drop walk frees the owned leaves, committed anonymous frames, and table frames with only a local reload.

capos-lib/src/mem_transition.rs models this ordering contract as a small state machine and, under a fault injected at the first, a middle, and the final commit step plus a rollback-step fault, proves the modelled world always reconciles PTE presence/permission, the tracking record, the virtual and frame-grant charges, frame ownership, and the deferred-free list – or fail-stops – never returning a silently inconsistent state. The tests also encode the pre-fix orderings (detach-metadata-before-PTE-removal, fallible rollback) and show the reconciliation predicate rejects the states they can produce, so the guarantee is not vacuous.

Code Map

• capos-lib/src/mem_failure.rs - host-testable MemoryExhaustion taxonomy: class-to-token/reason mapping and canonical exhaustion-message builder.
• capos-lib/src/mem_transition.rs - host-testable model of the transition failure-atomicity ordering contract (preflight/infallible-commit, infallible rollback, shootdown-gated deferred free) with fault-injection tests.
• capos-lib/src/vm_reservation.rs - host-testable anonymous reservation, borrowed-mapping provenance, and separate held-backing/borrowed-mapping charge model. Deliberately wrong overlap and wrong-object-unmap variants make its rejection and survival assertions non-vacuous.
• kernel/src/cap/mod.rs - memory_exhaustion_error builds the normalized overloaded capnp::Error for a MemoryExhaustion class.
• capos-lib/src/frame_bitmap.rs - host-testable physical frame bitmap core.
• capos-lib/src/cap_table.rs - capability holds and per-process ResourceLedger frame-grant accounting.
• capos-lib/src/frame_ledger.rs - bounded frame-grant helper retained for host tests.
• kernel/src/mem/frame.rs - Limine memory-map integration and global frame allocator wrapper.
• kernel/src/mem/heap.rs - kernel heap setup.
• kernel/src/mem/paging.rs - kernel remap, AddressSpace, page mapping, VM-cap page tracking, user copy helpers, and the infallible-after-preflight PTE primitives (unmap_present, protect_present, remap_present).
• kernel/src/mem/validate.rs - shared user-address arithmetic and bounds helper; page-table validation lives on the locked AddressSpace.
• kernel/src/cap/frame_alloc.rs - FrameAllocator capability and cleanup.
• demos/memoryobject-shared-parent/ and demos/memoryobject-shared-child/ - QEMU shared MemoryObject smoke.
• tools/qemu-memoryobject-shared-smoke.sh - transcript checks for the shared MemoryObject smoke.
• kernel/src/cap/virtual_memory.rs - VirtualMemory capability.
• kernel/src/spawn.rs - ELF, stack, and TLS user mappings.
• kernel/src/arch/x86_64/smap.rs - SMEP/SMAP setup and the direct-user-access guard; current user-buffer copies translate under the address-space lock and access frames through HHDM instead.

Validation

• cargo test-lib covers frame bitmap, frame ledger, ELF parser, cap-table pure logic, and the mem_failure memory-exhaustion taxonomy (every class is overloaded, tokens are stable and unique, messages carry their token).
• make run-untrusted-exhaustion forces the virtual-quota, physical-commit, result-cap-publication, and ProcessSpawner global-frame-pressure boundaries in QEMU and asserts each returns its typed token while an already-valid console call still completes. The global-pressure case runs through the proof-only run-untrusted-exhaustion-spawn-oom-fault sibling; the core pass continues to boot an ordinary QEMU kernel.
• cargo miri-lib runs host-testable capos-lib tests under Miri when installed.
• make kani-lib proves the bounded mandatory frame-bitmap, stale-handle, cap-slot/frame-grant accounting, and transfer preflight fail-closed invariants when Kani is installed.
• make run-smoke validates ELF mapping, process teardown, TLS, and clean shell-led halt.
• make run-spawn validates MemoryObject-backed FrameAllocator cleanup, VirtualMemory reserve/commit/decommit/VM_PROT_NONE/quota/release smoke, and runtime spawn checks.
• make run-memoryobject-shared validates a parent allocating and mapping a MemoryObject, typed refusal of an object map over a live anonymous reservation, typed refusal when a different object attempts the unmap, survival of the incumbent reservation and mapping after those refusals, transfer to a child, a child write through the same backing pages, clean unmap on both sides, and clean halt.
• make run-ipc-zerocopy validates the multi-message shared point-to-point buffer pattern at the substrate level: a producer transfers one MemoryObject to the consumer and then exchanges four record payloads through the shared mapping while endpoint CALLs carry only sequence numbers and checksums. This is a substrate proof, not the production data-plane shape: typed SharedBuffer with explicit producer/consumer ring metadata, notification primitives, and consuming service APIs (File.readBuf, BlockDevice.readBlocks, NIC RX/TX rings) are tracked under Open Work.
• make run-spawn validates ELF load failure rollback and frame exhaustion handling through ProcessSpawner.

Open Work

• Extend frame-grant accounting only if future DMA pinning or service-owned shared-buffer pools need authority beyond held MemoryObject caps and live borrowed mappings.
• Implement the accepted Shared Mapping Identity and Object Pins rules before shared WaitSet/ParkSpace or service-owned shared-buffer paths keep backing stable beyond a single locked copy/read. DMA retains its separate authority and quiesce contract.
• Add file, block, network, and DMA service APIs that use MemoryObject-backed SharedBuffer caps for zero-copy data paths.
• Add DMA isolation and device memory capability boundaries before userspace drivers.
• Add huge-page handling only with explicit ownership and teardown rules.