Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Memory Authority Model Backlog

This backlog turns Memory Authority Model into reviewable work. It does not replace the selected milestone (the loopyard project setting selected_milestone). Use it when a task touches memory authority, VirtualMemory, MemoryObject, SharedBuffer, pins, DMA, swap, OOM, or page-table mutation semantics.

Grounding

Project files read while creating this backlog:

  • docs/architecture/memory.md
  • docs/backlog/go-virtual-memory-contract.md
  • docs/proposals/oom-and-swap-proposal.md
  • docs/proposals/resource-accounting-proposal.md
  • docs/dma-isolation-design.md
  • docs/architecture/park.md
  • docs/architecture/scheduling.md
  • docs/architecture/userspace-runtime.md
  • docs/proposals/storage-and-naming-proposal.md
  • docs/proposals/go-runtime-proposal.md
  • docs/security/verification-workflow.md
  • docs/research/capability-systems-survey.md
  • REVIEW.md
  • loopyard board

Relevant research grounding:

  • docs/research/zircon.md
  • docs/research/genode.md
  • docs/research/sel4.md
  • docs/research/eros-capros-coyotos.md
  • docs/research/llvm-target.md

Validation Expectations

  • For docs-only slices, run a documentation build or the narrowest available link/check command; QEMU is not required unless behavior changes.
  • For implementation slices, add host tests, Kani, QEMU, or targeted instrumentation according to the proof table in the proposal.
  • Behavior changes should record concrete design grounding and verification evidence in the changed proposal, backlog, review note, or workplan entry.

Slice A: Memory-State Inventory

Goal: make current memory transitions auditable before changing behavior.

  • Inventory anonymous VM operations in kernel/src/cap/virtual_memory.rs and kernel/src/mem/paging.rs: reserve, commit, protect, decommit, unmap, address-space drop, and rollback.
  • Inventory MemoryObject operations in kernel/src/cap/frame_alloc.rs: allocation, result-cap publication, map, unmap, protect, cap release, borrowed mapping teardown, and result serialization rollback.
  • Inventory page-table mutation and TLB shootdown paths in kernel/src/mem/paging.rs, kernel/src/arch/, and scheduler residency tracking.
  • Inventory user-buffer validation/copy/read paths and classify which ones already hold the address-space stability guarantee.
  • Inventory ParkSpace cleanup interactions with VirtualMemory.unmap, VirtualMemory.decommit, MemoryObject.unmap, process exit, and future shared waiters.
  • Record a compact state-transition table in docs/architecture/memory.md or a follow-up design note.

The reader-facing inventory is in Memory Management: Current State-Transition Inventory. Its residual proof and design boundaries are concrete loopyard tasks for VM ownership host tests, shared mapping identity and pins, and SMP TLB/frame reuse; the failure-atomicity contract and the final MemoryObject release ordering are landed (see the note below).

Exit criteria:

  • The inventory names every current state transition, authority object, ledger, lock, and cleanup path relevant to user memory.
  • Any missing proof becomes a concrete backlog item rather than a vague TODO.

Landed from the inventory: the transition failure-atomicity contract (docs/architecture/memory.md, “Transition Failure Atomicity”). Anonymous decommit/unmap/protect and MemoryObject.unmap/protect are split into a fallible preflight (no mutation) and an infallible commit through AddressSpace::{unmap_present, protect_present, remap_present}, with an infallible protect rollback; the ordering contract is host-tested under fault injection in capos-lib/src/mem_transition.rs.

Also landed: the immediate ring drain now orders deferred TLB completions before deferred capability drops (cap_enter, service_sqpoll_snapshot), so a same-drain final MemoryObject.unmap + final CAP_OP_RELEASE returns the object’s frames to the allocator only after every remote shootdown acknowledgement. A cfg(qemu) guard in MemoryObjectBacking::drop asserts no completion is pending at free, and make test-memoryobject-final-release-ordering is a focused -smp 2 proof that force-marks a real sibling resident and shows the acknowledgement precedes allocator return and same-physical reuse. The broader SMP QEMU proof that a released anonymous frame is never reused while a stale remote TLB entry can still reach it is now landed too: the structural wait()-before-free in the drain_deferred_completions FreeFrame arm (with a cfg(qemu) removed-wait() tripwire) plus make test-tlb-frame-reuse-ordering (-smp 2) drive the shared unmap_present + defer_frame_free machinery VirtualMemory.decommit/unmap and commit rollback rely on (see Slice D and SMP TLB/frame reuse). The only Slice D item still open is huge-page frame teardown, gated on huge-mapping support.

Slice B: Host-Testable VM Ownership Model

Goal: move the parts of memory ownership that are pure logic into stronger host-test coverage where practical.

  • Decide whether sparse anonymous reservation interval logic should live in capos-lib or stay kernel-local with mirrored tests. Decision: stay kernel-local with mirrored tests. The interval set is inseparable from the AddressSpace (kernel/src/mem/paging.rs) that owns hardware page-table frames and per-page ShootdownCompletions, and that module has no host-test harness. The pure interval-set semantics and the reserve/commit/release charge lifecycle are mirrored and host-tested in capos-lib/src/vm_reservation.rs; the rationale doc comment lives there and at the cap-layer driver site kernel/src/cap/virtual_memory.rs.
  • Add tests for fixed no-replace hints, overlap rejection, middle reservation split, tail split, adjacent split behavior, and full-range release. (capos-lib/src/vm_reservation.rs tests.)
  • Add tests for committed-page bookkeeping under partial decommit and VM_PROT_NONE retained-frame accounting. (capos-lib/src/vm_reservation.rs.) Recommit zero-fill (a recommitted frame reading back zeroed) is a QEMU proof per docs/backlog/go-virtual-memory-contract.md item 8, not host-testable pure logic, so it is not re-scoped into this model.
  • Add tests for borrowed mapping provenance: anonymous reservations and object-backed mappings must not overlap, and object-specific unmap must reject a different backing object. Both rules were already enforced in AddressSpace: symmetric reservation/borrowed-page overlap checks and backing identity comparison through Arc::ptr_eq. The capos-lib::vm_reservation::BorrowedMappingLedger host model pins both rules with deliberately wrong variants, and make test-memoryobject-shared proves typed refusal plus mapping/reservation survival in-system.
  • Add ledger tests that virtual reservation and physical commit charges release exactly once on success, error, rollback, and process exit. (capos-lib/src/vm_reservation.rs Vm lifecycle tests, with a buggy double-release variant proving the balance predicate is non-vacuous.) Held-object-backing and borrowed-mapping charges are independent frame-grant categories: cap-table holds charge the backing pages they retain, while every live borrowed mapping charges the mapper until unmap. BorrowedMappingLedger host-tests their independent release; docs/architecture/memory.md records the production ledger and lifetime owners. (capos-lib/src/mem_transition.rs separately models the PTE-transition failure-atomicity of those unmap/protect paths.)

Exit criteria:

  • Pure memory ownership rules are tested without QEMU when they do not need hardware page tables. (cargo test-lib vm_reservation module.)
  • Any remaining kernel-only rule is documented with the reason it cannot be moved into host-testable logic. (Placement decision above and the capos-lib/src/vm_reservation.rs module doc.)

Slice C: Shared Mapping Identity and Pins

Goal: unblock future shared park words and real SharedBuffer APIs without using raw virtual addresses as authority.

  • Define the mapping identity record for MemoryObject-backed user pages: object id, object generation or backing epoch, page offset, mapping generation, address-space id, and address-space generation.
  • Decide whether shared waiters need explicit object pins, mapping pins, or a validation/use critical section around key derivation and wait registration.
  • Define how object pins are charged, released, and revoked, and which ledger owns the pin count or pinned page count.
  • Extend ParkSpace design only after shared key derivation can prove object identity and stale mappings cannot wake new owners.
  • Define service-owned SharedBuffer metadata for producer/consumer rings, notification, bounds, and role-specific permissions before file/network APIs consume it.

The first four contracts are recorded in Shared Mapping Identity and Object Pins. They are design only: SharedParkSpace, stable mapping records, object pins, and shared-buffer service metadata remain unimplemented.

Exit criteria:

  • Shared wait/wake and service-owned shared buffers have an object-identity rule that survives unmap, remap, transfer, release, and reuse.
  • Reviewers can reject any future shared-memory API that relies only on a raw user virtual address.

Slice D: TLB and Frame-Reuse Proof

Goal: make stale CPU observers part of the proof, not a local implementation assumption.

  • Identify all paths that remove or weaken PTEs and later free or reuse frames. Inventoried in docs/architecture/memory.md (“User memory state and authority” and “Page-table and TLB completion paths” tables plus the “Transition Failure Atomicity” narrative): the shootdown-gated frame frees (VirtualMemory.decommit/unmap, commit rollback of committed pages, and final MemoryObject backing release) all funnel through DeferredCompletionReservation::defer_frame_free / MemoryObjectBacking::drop; protect weakens PTEs but frees no frame; and the two direct-free paths that need no shootdown are the never-mapped commit-rollback frame and process-exit AddressSpace::drop.
  • Add targeted counters or QEMU diagnostics showing local flush and remote generation completion before frame return on an address space resident on multiple CPUs. The drain_deferred_completions FreeFrame arm frees only after wait() (which lexically precedes the free) returns, and a cfg(qemu) tripwire there prints ORDERING VIOLATION if that wait() is ever removed/weakened so a frame reaches the allocator before its remote acknowledgement. make test-tlb-frame-reuse-ordering (-smp 2) is the focused SMP proof; make test-memoryobject-final-release-ordering covers the final-release path. Both force a real online sibling resident and show same-physical reuse only after the acknowledgement.
  • Exercise VirtualMemory.decommit, VirtualMemory.unmap, VirtualMemory.protect, MemoryObject.unmap, process exit, and failed rollback under SMP where possible. test-tlb-frame-reuse-ordering drives the shared unmap_present + defer_frame_free + drain_deferred_completions machinery that decommit/unmap/commit-rollback all use; test-memoryobject-final-release-ordering covers MemoryObject.unmap + final release. protect frees no frame (only a deferred shootdown wait, no reuse), and process exit / never-mapped commit-rollback are the local-only cases recorded below rather than fake-proven under a synthetic resident sibling that never actually loaded the CR3.
  • Record which paths only need local flush because the address space cannot be resident remotely. Process-exit AddressSpace::drop and the never-mapped commit-rollback free are documented in docs/architecture/memory.md with the reasoning (external termination requires non-residency, and a CR3 switch-away evicts the non-global user translations of a departed address space; a never-installed frame is in no TLB).
  • Cover huge-page (1 GiB / 2 MiB) frame teardown when huge mappings are eventually introduced. Today the Drop for AddressSpace walk in kernel/src/mem/paging.rs (huge-page branches at lines 450 and 462) skips HUGE_PAGE PTEs with a TODO pass-through, so once huge pages are mapped into a user address space the backing 1 GiB / 2 MiB frames would leak on process exit. The work is blocked until huge-page support is added but must be filed against any branch that introduces huge user mappings.

Exit criteria:

  • A branch that changes page-table mutation can cite a proof that frames are not reused while stale TLB entries can still access them.

Slice E: OOM Boundary Normalization

Goal: make memory failures distinguish validation, quota, global pressure, and fatal execution failure.

  • Audit VirtualMemory, MemoryObject, FrameAllocator, and ProcessSpawner allocation failures for inconsistent failed vs overloaded behavior. Recorded in Memory Management (“OOM Boundary Normalization”): the frame-grant quota was failed in virtual_memory.rs but overloaded in frame_alloc.rs, and real physical OOM was failed while cap-table publication OOM was overloaded.
  • Define typed result or exception mapping for virtual quota exhaustion, physical commit exhaustion, global frame pressure, and result-cap publication failure. capos_lib::mem_failure::MemoryExhaustion maps all four to overloaded with a stable class token; the kernel constructs it through cap::memory_exhaustion_error at the VirtualMemory and MemoryObject/FrameAllocator boundaries.
  • Add hostile exhaustion tests for each allocation boundary that can be reached by an untrusted process. make test-untrusted-exhaustion forces the virtual-quota, physical-commit, result-cap-publication, and ProcessSpawner global-frame-pressure boundaries and asserts each typed token. The global-pressure pass is isolated in the proof-only test-untrusted-exhaustion-spawn-oom-fault sibling target; the core pass boots an ordinary QEMU kernel. cargo test-lib covers all four classes.
  • Route ProcessSpawner image-load allocation failures through the taxonomy. kernel/src/spawn.rs now returns typed image failures: physical-frame pressure maps to global-frame-pressure, construction bookkeeping stays an untokened overload, and internal invariants stay failed. Process/thread/run-queue construction quotas remain their distinct, uniformly overloaded resource family.
  • Add process-exit status design for future OOM page-fault termination.

Exit criteria:

  • Capability calls return predictable typed memory failures, and execution faults have an explicit lifecycle path rather than generic panic text.

The VirtualMemory, MemoryObject/FrameAllocator, and ProcessSpawner boundaries meet the typed-failure criterion. OOM page-fault termination remains open (above).

Slice F: DMA and Swap Preconditions

Goal: keep later device and swap work blocked on the memory model pieces they actually require.

  • Before userspace DMA drivers, implement or prove device-owner states, generation-checked handles, stale interrupt/completion handling, resident unswappable DMA pages, and scrub-before-reuse.
  • Before swap, define page eligibility bits, slot metadata, encrypted and authenticated page storage, per-boot keying, and faulting-process termination on restore failure.
  • Keep MemoryObject, shared IPC pages, ring/CapSet pages, secret pages, and DMA pages out of phase-1 swap unless a later proposal explicitly changes the model and adds proofs.

Exit criteria:

  • DMA and swap implementation branches have explicit prerequisite checklists and cannot merge by relying on generic frame ownership alone.