Memory-Model Audit

I1 Every physical frame has exactly one semantic owner in PMM.

I2 Every present MO-backed PTE is represented by a matching VmArea span and a matching MO ReverseMapEntry.

I3 Every ReverseMapEntry points to a live VSpace and a still-valid VA range.

I4 pmm_free() is called only after the last mapping reference is gone.

I5 mmsrv region metadata is a refinement of kernel VmArea state, not a competing second truth.

I6 rsrcsrv quota accounting must upper-bound, and ideally exactly match, actual kernel object memory usage.

I7 No two VmArea s in one VSpace overlap.

I8 map_mo / fork_range error paths leave no residual child-side PTE, VmArea, or reverse-map mutations attributable to the failed call.

I9 Kernel object sizing used by retype and quota accounting comes from one shared source of truth.

I10 Fork is child-atomic: success fully publishes child state, failure leaves the child in pre-call state.

I11 MmClient publication is atomic at the document’s abstraction level: no partially-swapped region/scalar state becomes observable.

I12 Policy code and kernel-VM code stay separated by an explicit layering boundary.

I13 Quota cost is idempotent: alloc-time charge equals free-time refund.

I14 Every kernel-side install performed by transactional fork is journaled exactly once before any later fallible step.

I15 The current mmsrv publication model assumes a single-threaded main loop.

I16 Fork dedup preserves aliasing only within the bounded dedup table design; above the bound it degrades to a documented caveat, not a clean proof story.

I17 After any COW-resolution path, the installed present PTE must correspond to a backing entry in the child MO radix tree and PMM owner state must agree with that child MO.

I18 If the kernel stores a raw physical address obtained from a Frame capability, it must also hold a kernel-side lifetime claim or rehome ownership before userspace can revoke the original capability.

I19 Any read of MemoryObject.pages that can race with commit/remove/grow must either hold commit_lock or use a separately-proved lock-free publication protocol.

I20 Every PMM-allocated page-table frame for a user VSpace must eventually return to PMM via pmm_free(...) with the matching owner tag.

Status: CLOSED

Area: VSpace map/fork metadata

Primary invariants: I2, I7, I8

overlap gate before metadata mutation;

maple reservation before insert;

reverse-map reservation ticket before commit;

infallible metadata commit after successful reservation.

Status: CLOSED

Area: MO reverse-map integrity

Primary invariants: I2, I3

dedicated MemoryObject::rmap_lock;

explicit lock order VSpace.lock -> MO.rmap_lock -> FRAME_LOCK;

snapshot + re-validate destroy walk to avoid inversion.

Status: CLOSED

Area: PMM safety

Primary invariants: I4

FrameAllocator::free_internal panics on non-zero map_count;

map_count widened to u32;

free-time diagnostics now report the failing frame and owner tag.

Status: CLOSED

Area: userspace VM mirror / fork publication

Primary invariants: I5, I10, I11, I14

transactional mmsrv::txn rollback guard;

staged region-table publication;

atomic commit-swap of region/scalar state;

layering split between policy and kernel-VM code.

Status: CLOSED

Area: quota sizing

Primary invariants: I6, I9, I13

shared object_alloc_bytes sizing helper;

compile-time kernel size assertions;

cached cost_bytes for idempotent refund;

removal of ad hoc rsrcsrv object-size logic.

Status: CLOSED

Area: COW resolve syscall path

Primary invariants: I17

new VSpace::cow_install_atomic helper (Reserve BUSY → Publish PTE+TLB+PMM mapping-refs → Finalize radix → Commit-point pmm_set_owner(MoData)) under MO.commit_lock;

resolve_cow_with_frame delegates to the helper; the child MO is resolved via the VSpace Maple tree before any allocation;

syscall_vspace_cow_resolve is an always-consume donation: inside one CAP_LOCK critical section it revokes the Frame cap and retags the PMM owner to KernelPrivate\{CowPool}, then calls the helper. Success flips it to MoData. Failure returns the phys to PMM via pmm_free(CowPool). A post-install revoke would have let CDT’s reclaim_child_range overwrite the MoData tag back to UntypedReserved and panic the next owner-mismatch check — the donation-style ordering avoids this.

Status: CLOSED

Area: COW pooled fast path

Primary invariants: I18

new KernelMetaKind::CowPool variant with per-subkind accounting;

VSPACE_SET_COW_POOL / VSPACE_REPLENISH_COW_POOL revoke each donated Frame cap and retag the backing frame to KernelPrivate\{CowPool} under CAP_LOCK + FRAME_LOCK;

VSpace::cleanup drains un-consumed pool entries via pmm_free(KernelPrivate\{CowPool}) before page-table teardown.

Status: CLOSED

Area: MO radix reader synchronization

Primary invariants: I19

resolve_page_depth and is_local_committed acquire commit_lock around every pages.get — per MO, never nested across two MOs.

self.cow_parent is read inside self.commit_lock so the cow_parent slot value observed by the reader is coherent with respect to the lazy-collapse writer.

The lazy-collapse branch of MemoryObject::destroy now writes remaining.cow_parent under remaining.commit_lock, closing the torn-field read/write race on the field itself.

The lingering writer sites in syscall_mo_resize, map_demand_*, and the map-path flatten step now acquire commit_lock around commit_page / pages.remove.

MemoryObject::commit_lock docstring and the global lock-ordering comment in kernite/src/mm/mod.rs now declare commit_lock at the same nesting depth as rmap_lock (disjoint), with explicit commit_lock -> ut.alloc_lock -> FRAME_LOCK ordering downstream.

Status: CLOSED

Area: COW fast-path atomicity

Primary invariants: I17

handle_cow_fault and handle_cow_fault_pooled both delegate to cow_install_atomic; the helper’s Reserve step uses RadixTree::reserve_slot(BUSY) so radix-alloc failure returns the frame to PMM without ever touching PTE or PMM owner state;

write_entry failure rolls back the BUSY reservation;

RaceLost (another CPU already resolved) is reflected back to the fault handler as "continue", with the donated / allocated frame released with its current tag (KernelPrivate\{General} or KernelPrivate\{CowPool}).

Status: CLOSED

Area: VSpace teardown

Primary invariants: I20

free_pdpt_recursive / free_pd_recursive call pmm_free(KernelPrivate\{PageTable}) on each PDPT, PD, and PT frame after the self-mapping ref is released via pmm_release_mapping;

PML4 / aarch64 L0 root continue to be owned by the parent untyped carve and are intentionally skipped;

applies unchanged on both x86_64 and aarch64 (the teardown helpers share one arch-generic 4-level walk).

COW parent lifetime. Child MOs reference their parent through an internal cap slot and a manually-maintained refcount instead of a uniform CDT-managed lifetime.

Multiple mapping views. A single region is tracked in three places: PMM map_count, kernel VmArea / ReverseMapEntry, and userspace MmRegion. Consistency is invariant-level, not structural.

Bounded fork dedup. DEDUP_MAX = 16 caps alias preservation; beyond that the guarantee degrades to a documented caveat.

Intermediate radix nodes on write_entry failure. cow_install_atomic removes the BUSY leaf on rollback but does not compact intermediate nodes allocated during Reserve. Memory accounting only; readers see the slot as uncommitted, and MO teardown frees the nodes.

Pool depth drift on RaceLost. handle_cow_fault_pooled consumes the pool entry before calling cow_install_atomic. A RaceLost frees the consumed frame via pmm_free(CowPool) without emitting a notification-ring entry, so mmsrv sees the deficit only at the next replenish. Correctness-neutral (another CPU already committed) but counter-visible.

First-mapping caller lifetime. resolve_page_depth's returned phys has map_count >= 1 only for callers already holding a mapping to the page. First-mapping callers (map-syscall initial install) must finish the PTE install inside the same VSpace.lock window; otherwise concurrent unmap from other VSpaces could drop map_count to zero and free the frame. All current callers satisfy this, but the window is narrow rather than absent. A tighter claim (incrementing map_count inside resolve_page_depth) is tracked as follow-up.

cow_parent slot-reuse window. H8 serializes the write of cow_parent under the child’s commit_lock, so the reader observes a coherent slot value. But the reader releases commit_lock before calling deref_cow_parent(old_slot); in the window between unlock and deref, the CDT may free and reallocate that slot to an unrelated cap. Today this is bounded by A1 (kernel objects never freed — the underlying MO storage is stable) plus the fact that deref_cow_parent type-checks ObjectType::MemoryObject before returning the pointer. A stricter closure (holding commit_lock across the deref, or gating parent-chain walks behind CAP_LOCK) is tracked as follow-up.

handle_cow_fault behavior change. When the faulting VA has a COW-bit PTE but the Maple-tree VMA lookup does not yield a backing MO, the function now returns Err(VSpaceError::NotMapped) instead of the previous silent-success path (which was itself the O1 bug). This is intentional and necessary for I17, but any user-visible code that relied on the silent-success behavior will now see the fault dispatcher’s error path (SIGSEGV-equivalent). The existing test_runner fork / mmap modules exercise COW; a just run pass is the empirical check that no legitimate caller regresses.

kernel objects are carved from untyped memory;

backing bytes are not reused during normal object destruction paths.

raw *mut VSpace / *mut KernelObject identity is used in reverse-map and destroy logic;

snapshot + re-validate reasoning depends on pointer stability;

ABA is ruled out by design rather than by generation tagging.

any future object-memory reuse path;

any typed-object free-and-reallocate design;

any move away from monotonic untyped-backed object storage.

MmClient publication uses staged swap, not SMP-safe publication.

I10 and I11 currently rely on the absence of concurrent readers/writers on the same MmClient;

the current commit-swap protocol is not an RCU or seq-lock design.

adding worker threads to mmsrv;

splitting policy handling across concurrent server threads;

introducing partial atomic publication of only some MmClient fields.

Method: static source audit + targeted code walkthrough of the landed cow_install_atomic primitive and its three fault-path callers.

Result: O1-O5 closed, recorded as H6-H10.

Main landed fix themes: atomic 3-way COW transaction (PTE / MO radix / PMM owner), kernel-owned COW scratch pool via KernelPrivate\{CowPool}, radix reader / writer synchronization via commit_lock, user-VSpace page-table reclamation.

Build / boot verification pending — recorded as a near-term obligation.

Method: static source audit only

Result: current HEAD is not proof-ready

Recorded blockers: O1-O5

Main regression themes: COW materialization, raw frame lifetime, radix synchronization, page-table reclamation

Method: static audit plus code review of landed fixes

Result: H1-H5 closed

Main landed fix themes: metadata reservation, reverse-map locking, PMM free hardening, mmsrv transactionality, quota sizing SSOT