# Memory Authority Model Backlog This backlog turns [Memory Authority Model](../proposals/memory-authority-model-proposal.md) 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.