Proposal: Memory Authority Model

capOS already has implemented memory management. This proposal defines the missing cross-cutting contract: which capability may create or hold memory, which memory may move or be reclaimed, when a mapping mutation is complete, and which proofs are required before shared-memory, DMA, swap, and language-runtime features build on that substrate.

This is deliberately not a CPU or language memory-ordering model. Atomic ordering, cache coherence, and Rust aliasing rules remain their own topics. This page covers OS memory authority, residency, consistency, and lifecycle.

Related

• Memory Management documents current physical frames, address spaces, user-buffer validation, VirtualMemory, and MemoryObject.
• Go VirtualMemory Contract freezes the reserve/commit/decommit contract this proposal treats as the current anonymous-memory baseline.
• OOM Handling and Swap owns memory-pressure, OOM, reclaim, and encrypted swap policy.
• Resource Accounting and Quotas owns the one-ledger-of-record and reserve/commit/rollback/release vocabulary.
• DMA Isolation owns device-visible memory, IOMMU, stale DMA, and scrub-before-reuse requirements.
• Park Authority records why shared park words need mapping identity or object pins before they can be safe across processes.
• Memory Authority Model Backlog decomposes the research, design, and proof work behind this proposal.

Problem

The current tree has strong local rules, but they are spread across several documents and implementations:

• anonymous VirtualMemory ranges separate reservation from physical commit;
• MemoryObject caps can be shared and mapped into multiple address spaces;
• user-buffer copies validate and use pointers while holding the address-space lock;
• TLB shootdown is routed through address-space residency masks;
• private ParkSpace cleanup handles anonymous unmap/decommit and explicit MemoryObject.unmap;
• DMA isolation requires resident unswappable pages, generations, quiesce, and scrub-before-reuse;
• OOM policy rejects default overcommit and forbids an ambient OOM killer.

Those rules are individually useful, but future work needs a single answer to questions such as:

• Is this page only reserved, physically committed, resident, pinned, swapped, or device-visible?
• Which cap or ledger is the authority that made it that way?
• Can this backing frame be reclaimed, unmapped, shared, donated, or exposed to a device?
• When is it safe to reuse a frame after unmap, decommit, protect, process exit, revoke, or failed rollback?
• Which proof must exist before a shared park word, NIC ring, block buffer, Store blob, GPU buffer, Go heap arena, or swap slot depends on the rule?

Without a consolidated contract, later features can accidentally treat MemoryObject, SharedBuffer, DMA pool pages, anonymous VM pages, and swapped pages as interchangeable. They are not interchangeable authority classes.

Design Grounding

The project grounding for this proposal is:

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

Relevant research grounding:

• docs/research/zircon.md for VMO/VMAR separation, mapping authority, and VMO commit/decommit precedent.
• docs/research/genode.md for parent-routed sessions and resource quota discipline.
• docs/research/sel4.md for explicit authority, no ambient allocation authority, and the proof value of small stable object invariants.
• docs/research/eros-capros-coyotos.md for single-level-store and keeper lessons; capOS should not make transparent persistence or implicit paging the baseline by accident.
• docs/research/llvm-target.md for Go/runtime memory hooks that require reserve, commit, decommit, and fault behavior.

Goals

1. Define the authoritative state vocabulary for user memory, shared memory, pinned memory, DMA memory, and future swapped memory.
2. Make every memory-state transition name the capability and ledger that authorizes it.
3. Specify when validation, mapping mutation, TLB shootdown, cleanup, and frame reuse are complete.
4. Keep future SharedBuffer, file, network, GPU, and DMA paths from bypassing MemoryObject provenance or residency rules.
5. Tie memory-pressure and OOM behavior to explicit budgets and process lifecycle, not allocator surprises.
6. Convert this contract into host tests, QEMU smokes, Kani models, and review gates.

Non-Goals

• No demand paging or swap implementation in this proposal.
• No transparent global persistence or EROS-style single-level store.
• No copy-on-write clone design.
• No sub-VMAR or nested address-region capability in the first version.
• No generic userspace pager in the page-fault path.
• No change to CPU atomic ordering, language memory models, or Rust aliasing rules.

Memory Authority Classes

The model starts by naming memory by authority and residency, not by how it is convenient for one subsystem to access it.

Two rules follow from this table:

• A capability that maps CPU-visible bytes does not automatically grant device visibility, swap eligibility, pin authority, or persistence.
• A residency promise is an authority and accounting event, not a flag that a helper may set opportunistically.

State Machines

Anonymous VirtualMemory

Anonymous memory follows this lifecycle:

1. unreserved
2. reserved
3. committed inaccessible (VM_PROT_NONE) or committed accessible
4. decommitted reserved
5. unreserved

Required properties:

• reserve charges virtual reservation and installs no present user PTE.
• commit is all-or-nothing: frame allocation, ledger charge, page-table mutation, committed-page metadata, and deferred TLB completion reservation either all become visible or all roll back.
• protect changes accessibility only for committed pages; it does not create backing.
• decommit releases committed frames and physical charges while preserving virtual reservation.
• unmap releases the reservation and any committed backing inside it.
• ring and CapSet virtual ranges remain outside caller-controlled VirtualMemory operations.

MemoryObject

MemoryObject backing has a separate lifecycle from any one mapping:

1. allocated by FrameAllocator
2. held through one or more process cap-table entries
3. borrowed into one or more address spaces by MemoryObject.map
4. unmapped or torn down from those address spaces
5. released after the final cap and final borrowed mapping drop their holds

Required properties:

• held MemoryObject caps charge holder frame-grant pages;
• each borrowed mapping charges the mapper while it remains mapped;
• object-backed pages are tracked separately from anonymous reservations;
• unmap/protect must prove the affected range is backed by the same object;
• releasing a cap cannot leave uncharged live mapped backing behind;
• future direct read/write, slice, clone, file-backed, or DMA-backed subclasses must define how they differ from the current physically backed object.

Pinned and Device-Visible Memory

Pinned memory is not just a mapped page with a refcount. It is a promise that reclaim, swap, and frame reuse will not move or free the page until the pin is released.

The first reusable state machine should be:

1. resident
2. pin_reserved
3. pinned
4. pin_draining
5. resident

DMA-visible memory extends this with device ownership:

1. allocated
2. mapped_to_device
3. submitted
4. quiescing
5. device_mapping_removed
6. scrubbed
7. released

The device state machine must advance generations or epochs before reuse so stale handles, stale interrupts, and stale completions fail closed.

Future Swap

Swap is a later extension of committed anonymous memory:

1. committed resident
2. eviction reserved
3. encrypted slot written and authenticated
4. committed swapped
5. faulting restore
6. committed resident

No phase-1 swap path may include MemoryObject backing, shared IPC pages, ring/CapSet pages, DMA pages, kernel metadata, or secret pages. If swap-in cannot restore data or authenticate the slot, the faulting process exits with a typed OOM or corruption reason; the kernel must not fabricate contents.

Mapping Consistency

The consistency rule is:

A frame may return to the allocator, be exposed to a different authority, or be made device-visible only after every stale CPU and device observer has been invalidated or made irrelevant by generation.

For current CPU mappings this means:

• address-space mutation holds the address-space lock while checking and changing metadata;
• local page-table changes flush locally before returning to user mode;
• remote CPUs that have run the address space receive and acknowledge the required TLB shootdown generation before freed frames can be reused;
• cleanup paths reserve deferred completion slots before mutation when they may need to free frames after shootdown;
• private ParkSpace waiters are interrupted before an unmapped virtual address can be reused for unrelated state.

For future shared keys, DMA, and swap this means:

• shared park keys must be derived from MemoryObject identity and offset, or the backing object must be explicitly pinned for the duration of key derivation and wait registration;
• DMA page reuse requires descriptor quiesce, interrupt/completion generation checks, IOMMU or bounce-buffer invalidation, and scrub-before-release;
• swapped pages carry slot generation/integrity metadata, and stale slots must not be accepted as current backing.

Accounting Rules

Every state transition must name exactly one ledger of record:

• virtual reservation pages: process/address-space VM ledger;
• anonymous committed pages: process frame-grant or future memory-commit ledger;
• held MemoryObject backing: holder frame-grant ledger;
• borrowed MemoryObject mappings: mapper frame-grant ledger plus address-space tracking;
• pinned pages: future pin ledger owned by the pinning authority;
• DMA pool bytes, DMA buffers, descriptors, MMIO mappings, interrupt holds, and in-flight DMA submissions: device-manager ledger;
• swap commitment and swap slots: future swap/budget ledger;
• kernel metadata: kernel capacity budget until explicit object funding exists.

Status views, metrics, and audit logs may mirror these values, but they are not allowed to grant or deny resources from stale copies.

Failure Semantics

Capability-call boundaries return controlled failures:

• malformed ranges, overflow, unsupported protection, and authority mismatch return deterministic validation errors;
• local budget exhaustion returns quota denial or typed OOM;
• global pressure may attempt reclaim first if the memory class is eligible;
• rollback failure enters a bounded recovery or emergency path rather than publishing half-mutated authority.

Execution faults are process lifecycle events:

• access to unreserved memory is an ordinary fault;
• access to reserved uncommitted memory is a reservation fault, not implicit demand commit;
• access to committed VM_PROT_NONE is a protection fault;
• future failed swap-in or failed zero-fill terminates the faulting process, not a random victim.

Boot-time core allocation failures remain boot-fatal until capOS moves kernel object memory under explicit authority.

Proof Obligations

Before a feature depends on this model, it must add or cite the relevant proof:

Kani should stay focused on bounded pure primitives in capos-lib. Hardware-dependent behavior such as TLB shootdown, page faults, and DMA requires QEMU or targeted integration evidence.

Phasing

Phase 0: Contract and Inventory

• Land this proposal and the backlog.
• Inventory existing memory-state transitions and match them to the classes above.
• Identify code paths whose errors currently blur validation failure, quota denial, and global pressure.

Phase 1: Host-Testable Ownership Model

• Extract or mirror sparse anonymous reservation behavior into host-testable logic where useful.
• Add model tests for reservation split/merge, committed-page bookkeeping, borrowed mapping provenance, and one-ledger-of-record accounting.

Phase 2: Shared-Memory Provenance and Pins

• Define MemoryObject mapping identity sufficient for SharedParkSpace, service-owned shared buffers, and zero-copy file/network paths.
• Add explicit object pins or mapping pins only where a locked copy/read is not enough.

Phase 3: Runtime Budgets and OOM Normalization

• Add spawn-time memory budget policy once the selected milestone sequence reaches resource-profile work.
• Normalize allocation failure results at capability boundaries.
• Add typed process exit reporting for memory faults and future OOM.

Phase 4: DMA and Swap Extensions

• Treat userspace drivers as blocked until DMA owner states, generations, ledgers, and stale-completion proofs exist.
• Treat swap as blocked until page classes, slot metadata, encryption, and fault lifecycle are explicit.

Open Questions

1. Should capOS expose a first-class pinned-memory option on VirtualMemory, or only through narrower future caps such as SharedParkSpace, DMAPool, and SecretMemory?
2. Should MemoryObject gain direct read/write and slice operations before file/network SharedBuffer APIs, or stay mapping-only until a concrete service needs the API?
3. Which pure address-space interval logic should move into capos-lib for Kani/host testing without dragging in architecture-specific page-table details?
4. What is the smallest status surface that exposes reservation, commit, resident, pinned, borrowed, DMA, and swapped counts without creating a second enforcement counter?
5. How much kernel metadata should remain permanently reserved before capOS adds explicit object-funding authority for kernel allocations?

Bottom Line

capOS should treat memory state as capability authority plus ledgered residency. Anonymous reservations, committed frames, shared objects, pins, DMA pages, and swapped pages need distinct contracts. The near-term path is not to implement swap or a pager; it is to make the authority, accounting, TLB/device-observer, cleanup, and proof rules precise enough that future shared-memory and device work cannot accidentally bypass them.