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 in WORKPLAN.md. 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.md
  • REVIEW.md
  • REVIEW_FINDINGS.md

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.

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.

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.
  • Add tests for fixed no-replace hints, overlap rejection, middle reservation split, tail split, adjacent split behavior, and full-range release.
  • Add tests for committed-page bookkeeping under partial decommit, VM_PROT_NONE protect/restore, and recommit zero-fill assumptions.
  • 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.
  • Add ledger tests that virtual reservation, physical commit, held object backing, and borrowed mapping charges release exactly once on success, error, rollback, and process exit.

Exit criteria:

  • Pure memory ownership rules are tested without QEMU when they do not need hardware page tables.
  • Any remaining kernel-only rule is documented with the reason it cannot be moved into host-testable logic.

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.

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.
  • Add targeted counters or QEMU diagnostics showing local flush and remote generation completion before frame return on an address space resident on multiple CPUs.
  • Exercise VirtualMemory.decommit, VirtualMemory.unmap, VirtualMemory.protect, MemoryObject.unmap, process exit, and failed rollback under SMP where possible.
  • Record which paths only need local flush because the address space cannot be resident remotely.

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.
  • Define typed result or exception mapping for virtual quota exhaustion, physical commit exhaustion, global frame pressure, and result-cap publication failure.
  • Add hostile exhaustion tests for each allocation boundary that can be reached by an untrusted process.
  • 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.

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.