Shared Mapping Identity and Object Pins

This note defines the identity and lifetime contract needed before capOS can implement SharedParkSpace or expose a production SharedBuffer API. It does not add either behavior. The contract keeps a raw virtual address from becoming cross-process authority and gives unmap, remap, revocation, and backing reuse distinct generations that future code can check.

Current Boundary

The current MemoryObject implementation provides real shared backing, but not stable mapping provenance:

• MemoryObjectBacking stores only phys_addr and page_count and is retained by Arc references from caps and borrowed mappings.
• AddressSpace::record_borrowed_vm_range records one UserPageMapping per page. Each record contains only a virtual address and an Arc<dyn BorrowedFrameOwner>; AddressSpace::owns_borrowed_vm_range_from proves ownership with Arc::ptr_eq.
• AddressSpace has no explicit address-space id, address-space generation, or mapping-generation allocator.
• MemoryObjectCap::map, MemoryObjectCap::unmap_region, and MemoryObjectCap::protect hold the address-space lock while checking and changing borrowed-mapping metadata and PTEs. This is the stability boundary the future provenance lookup must preserve.
• CapTable::insert_with_epoch derives CapHold.object_id from the address of a CapObject. That value is valid for current capability-slot revocation but is not a backing id: a derived SharedParkSpace is a different CapObject, and allocator reuse may eventually reuse a pointer value.
• ParkSpaceCap is stateless process-local submit authority. sched::park, sched::unpark, and Process::park_waiters use only the caller’s process generation and uaddr. SharedParkSpace is a marker in the schema and capos-rt; the kernel does not dispatch shared waits or wakes.

Consequently, current pointer equality remains sufficient for MemoryObject.unmap and protect, but it must not be serialized, exposed, or used as a future shared-park key.

Identity Records

The kernel will assign nonzero, boot-lifetime ids and generations. A counter that would wrap is retired; it is never wrapped to a value that could alias a stale record.

#![allow(unused)]
fn main() {
struct MemoryObjectIdentity {
    object_id: u64,
    backing_epoch: u64,
}

struct AddressSpaceIdentity {
    address_space_id: u64,
    address_space_generation: u64,
}

struct SharedMappingIdentity {
    object_id: u64,
    backing_epoch: u64,
    object_page_offset: u64,
    mapping_generation: u64,
    address_space_id: u64,
    address_space_generation: u64,
}
}

The fields have separate jobs:

MemoryObjectBacking owns the current MemoryObjectIdentity and its lifecycle state. Every authority wrapper derived from it, including MemoryObjectCap and the future SharedParkSpaceCap, stores an immutable observed_backing_identity snapshot alongside the backing Arc. Cap transfer copies the same wrapper and snapshot; deriving a different wrapper copies the snapshot while holding the backing lifecycle lock. No operation substitutes a CapHold.object_id or wrapper pointer for this identity.

AddressSpace owns AddressSpaceIdentity and a non-wrapping next-mapping-generation counter. UserPageMapping is replaced or extended with SharedMappingIdentity plus its existing backing reference. Recording the object page offset makes identity independent of contiguous physical allocation and therefore compatible with a later non-contiguous or pageable backing representation.

The mapping record is kernel metadata. It is not a transferable token and does not itself authorize map, read, write, wake, pin, DMA, or persistence.

Mapping Publication and Removal

MemoryObjectCap::map allocates one mapping generation after range, quota, and tracking preflight succeeds but before it publishes borrowed-mapping records. For page i of a mapping whose byte offset is page-aligned, the record stores object_page_offset = offset / PAGE_SIZE + i. Publication remains under the same AddressSpace lock as the PTE installation and rollback.

The following rules apply:

• a partial map failure publishes no mapping identity;
• result-serialization rollback removes every record bearing that map’s generation along with its PTEs;
• protect may change PTE permissions but not identity;
• partial unmap removes only the affected per-page records; surviving pages retain their original mapping generation;
• mapping the range again, even to the same backing and offset, allocates a new mapping generation;
• AddressSpace::drop invalidates the address-space generation before its mapping records and backing references can be reused.

These rules preserve the current failure-atomic mapping contract in MemoryObjectCap::{map,unmap_region,protect} and AddressSpace::{record_borrowed_vm_range,forget_borrowed_vm_range_from}.

Shared-Key Derivation

A future SharedParkSpace contains a reference to one MemoryObjectBacking and the immutable backing identity observed when the cap was derived. It grants shared park/wake authority for that backing; it does not grant memory access or the right to select another backing by id.

For a 4-byte-aligned user address uaddr, shared wait and wake derive a key as follows:

1. Resolve the SharedParkSpace cap and retain its observed_backing_identity. This is an early rejection only; admission performs the authoritative epoch check below.
2. Hold the caller’s AddressSpace lock across PTE validation, mapping-record lookup, and the wait-word read when the operation is a wait.
3. Require the word to be readable, contained in one present 4 KiB borrowed page, and backed by the same (object_id, backing_epoch) as the SharedParkSpace.
4. Compute byte_offset = object_page_offset * PAGE_SIZE + (uaddr & (PAGE_SIZE - 1)) with checked arithmetic. Reject misalignment or an offset whose 4-byte word exceeds the object size.
5. Prepare the process pin-ledger charge and reserved waiter/CQE capacity, then acquire the backing’s shared-park state lock while the scheduler and address-space locks remain held. Under that lock, recheck that the lifecycle is open and that the wrapper snapshot, mapping record, and current backing identity are identical. Atomically convert the prepared charge into an active ObjectPin and publish the waiter in the backing-owned bucket.
6. Retain the complete SharedMappingIdentity as waiter provenance, but use only the following equality key:

#![allow(unused)]
fn main() {
ParkKey::Shared {
    object_id,
    backing_epoch,
    byte_offset,
}
}

mapping_generation and address-space identity are deliberately absent from key equality. Two mappings of the same backing offset in different address spaces must converge. They remain in waiter provenance so unmap and teardown can cancel only waiters admitted through the removed mapping generation.

A shared wake repeats the same mapping validation. Supplying the right offset through a mapping of a different object, a stale epoch, an anonymous mapping, or an old mapping generation fails closed before looking up a waiter bucket.

The lifecycle recheck and publication are the admission linearization point. Every failure before it releases the prepared pin charge, waiter slot, and CQE credit. After it succeeds, revocation must observe and drain the published waiter. There is no state in which an old-epoch pin is live but absent from the registry revocation scans.

Canonical Waiter Registry

Exactly one bounded SharedParkRegistry belongs to a MemoryObjectBacking and its current epoch. It is not stored in an individual SharedParkSpaceCap. All independently derived caps for the same backing epoch refer through their backing Arc to this registry, so equal ParkKey::Shared values always select the same bucket namespace.

The first implementation reserves the fixed registry and bucket metadata once as part of making the backing SharedParkSpace-eligible. That storage is charged to the backing object’s fixed metadata budget, not to whichever derived cap is used first. Later derived caps allocate no second registry. Revocation closes and drains the epoch’s registry; backing destruction releases the storage only after all caps, mappings, and waiter pins are gone.

Pin Choice

Shared waits use an explicit object pin plus a validation/use critical section. They do not use a mapping pin.

The address-space lock closes the race between mapping validation and waiter registration: registration either observes the live mapping record or loses to its removal. The object pin then retains the backing identity and the object-owned waiter bucket after the address-space lock is released. A mapping pin would unnecessarily prevent ordinary unmap for the entire wait duration and would make a blocked thread an implicit virtual-address-layout authority.

Each shared waiter stores an ObjectPin containing:

• an Arc<MemoryObjectBacking>;
• the (object_id, backing_epoch) it pinned;
• the waiting process’s aggregate pin-account token;
• the full SharedMappingIdentity used to admit the wait.

Current MemoryObject backing is resident and unswappable, so this object pin is initially a lifetime and provenance guarantee, not DMA authority. A future pager must treat a live object pin as a no-reclaim promise; a future DMA path still requires the separate DMAPool quiesce, generation, and scrub contract.

Pin Accounting

Pinned pages are a distinct resource class with one ledger of record. The waiting process owns a bounded pin ledger keyed by (object_id, backing_epoch). The first waiter from that process to that backing charges MemoryObjectBacking::page_count; additional waiters from the same process and epoch increment a bounded waiter refcount without charging the same pages again. The last such waiter releases the page charge.

This whole-backing charge is intentional: the current backing is one allocation behind one Arc, so a pin on any page retains every page. If backing lifetime later becomes page-granular, the ledger may charge only the retained page span without changing shared-key identity.

The pin ledger is separate from the current cap-table frame_grant_pages ledger because cap holds, borrowed mappings, and waiter pins are distinct live authorities with different release paths. Status surfaces may aggregate them, but neither may authorize from a mirrored total. Pin-account entries, waiter slots, and object buckets are fixed-capacity or pre-reserved; park, wake, timeout, cancellation, and exit do not allocate.

The existing per-thread waiter bound and reserved CQE credit remain charged to the waiting process. The one backing-owned registry is charged once when the backing becomes SharedParkSpace-eligible, as required by the Park authority contract; deriving another cap or touching a new offset cannot allocate a second or unbounded bucket namespace.

Release, Unmap, and Revocation

Pin ownership follows the waiter, not the cap slot that submitted it:

• value mismatch, zero timeout, invalid mapping, quota denial, or full object bucket enqueue no waiter and leave no pin charge;
• successful registration transfers one prepared pin token into the waiter;
• wake, timeout, explicit cancellation, mapping-generation removal, thread exit, and process exit each consume the waiter and release its token exactly once;
• if CQE delivery must be retried, the waiter first leaves the shared-key bucket and becomes a completion-only record. The pin can then be released because retry state contains no reusable shared key;
• release of the last SharedParkSpace cap removes submit authority but does not invalidate already registered waiters or free their storage;
• MemoryObjectBacking cannot be destroyed while any waiter pin retains it.

Unmap records the removed SharedMappingIdentity values. Shared-wait cleanup matches the full provenance tuple, so removing one alias cancels only waiters registered through that mapping generation; waiters admitted through another address space or alias remain eligible for a wake on the same shared key. A later remap at the same virtual address has a different mapping generation and cannot inherit the removed waiters.

Explicit backing revocation is stronger:

1. Acquire scheduler state and then the backing’s combined lifecycle/registry lock. Mark the current epoch closing and advance backing_epoch; this is atomic against the final admission recheck and waiter publication.
2. Drain every object bucket for the old (object_id, backing_epoch) and turn its waiters into PARK_INTERRUPTED completions, or silently consume them for exiting processes.
3. Release each old-epoch pin token exactly once.
4. Reject old SharedParkSpace park/wake and old MemoryObjectCap info, map, protect, and derive operations by comparing their immutable snapshot with the backing. An old MemoryObjectCap may invoke only identity-matched unmap cleanup for mappings it created, plus ordinary cap release; cleanup cannot create a mapping, pin, or shared key.
5. Reuse backing storage or physical frames only after old pins, mappings, and required TLB completions are gone.

Epoch exhaustion retires the backing identity rather than wrapping. Revocation does not rely on a physical address, virtual address, Arc pointer value, or cap-slot generation.

The first implementation treats backing revocation as terminal: it does not mint a post-revoke current MemoryObjectCap or reopen the same backing. A future reissue operation would need separate authority and would have to mint every wrapper with the then-current snapshot under the lifecycle lock after the old registry is drained. That reissue operation is outside this contract.

Race Outcomes

The implementation lock order is cap table -> scheduler -> address space -> backing lifecycle/registry for shared park admission. The final epoch check, conversion of a prepared pin charge, backing active-pin increment, and waiter publication occur under the last lock. Revocation uses cap table -> scheduler -> backing lifecycle/registry when entered from capability dispatch, or scheduler -> backing lifecycle/registry from kernel cleanup. It never acquires an address-space lock while holding the backing lock. Unmap captures provenance under the address-space lock and performs waiter cleanup after releasing it. All admission failures roll back their prepared process pin charge and reserved CQE/waiter capacity before releasing scheduler state.

Implementation and Proof Handoff

The implementation slice must update these symbols or their replacements:

• MemoryObjectBacking, MemoryObjectCap::map, and MemoryObjectCap::unmap_region in kernel/src/cap/frame_alloc.rs;
• AddressSpace, UserPageMapping, and the borrowed-range helpers in kernel/src/mem/paging.rs;
• ParkSpaceCap/the future SharedParkSpaceCap in kernel/src/cap/park_space.rs;
• ParkWaitRecord, Process::park_waiters, sched::park, sched::unpark, and the unmap/exit cleanup paths in kernel/src/process.rs and kernel/src/sched.rs;
• compact park dispatch in kernel/src/cap/ring.rs, without changing the raw virtual address into a cross-process key.

Required tests include alias convergence through two independently derived SharedParkSpace caps, same-address/different-object separation, object-epoch reuse rejection, mapping-generation cancellation, address-space teardown, cap release with a live waiter, revoke racing wait and wake, and exact aggregate pin charge/release on every terminal path. A focused model must pause admission after initial cap resolution, revoke the backing, then prove the final epoch check refuses publication and rolls back every reservation. A QEMU shared-park proof must show two processes mapping the same MemoryObject at different virtual addresses and rendezvousing through independently derived caps backed by the one canonical registry.

Design Grounding

Current project authority and implementation:

• Memory Management
• Park Authority
• Memory Authority Model
• Memory Authority Model Backlog
• kernel/src/cap/frame_alloc.rs
• kernel/src/mem/paging.rs
• kernel/src/cap/park_space.rs
• kernel/src/process.rs
• kernel/src/sched.rs
• capos-lib/src/cap_table.rs

Relevant prior-art summaries:

• Fuchsia/Zircon grounds the separation between a memory object and its per-address-space mappings.
• Genode grounds explicit, bounded resource donation and accounting for shared-memory objects.