# 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.

```rust
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:

| Field | Meaning and allocation rule |
| --- | --- |
| `object_id` | Names one `MemoryObjectBacking`, independent of any cap slot, wrapper object, physical address, or virtual address. It is allocated when the backing is created and is never reused during the boot. |
| `backing_epoch` | Names the live revocation generation of that backing. It starts nonzero and advances before explicit backing revocation drains derived authority. Reclaiming and reusing physical frames cannot preserve the old pair. |
| `object_page_offset` | Page index within the backing for this PTE. It is recorded directly; it is not reconstructed from a physical address. |
| `mapping_generation` | Names one successful `MemoryObject.map` publication in one address space. All pages installed by that call receive the same generation. `protect` preserves it; an unmapped then remapped range receives a new generation. |
| `address_space_id` | Names an `AddressSpace`, not a PID or CR3 frame. The current one-address-space-per-process model may initially allocate it alongside the process, but the stored type must not assume that relationship. |
| `address_space_generation` | Distinguishes teardown and reuse of an address-space id. It changes before an old address space can be replaced under the same id. |

`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:

```rust
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

| Race | Required result |
| --- | --- |
| shared wait vs unmap | Either registration completes with the old mapping provenance and unmap cancels that waiter, or unmap removes the record first and registration fails. |
| shared wait vs backing revoke | Either the pin is admitted in the old epoch and revoke drains it, or the epoch closes first and admission fails. |
| shared wake vs alias unmap/remap | Wake derives from its own live mapping. It can wake only the matching backing epoch and byte offset; removed mapping provenance cannot be mistaken for the new mapping. |
| final cap release vs blocked waiter | Cap submit authority disappears, but the waiter-owned pin retains the backing and bucket until a terminal waiter path. |
| physical frame reuse | A new backing receives a different object id, or a surviving backing has a different epoch. An old shared key never aliases the reused frame. |

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](memory.md)
- [Park Authority](park.md)
- [Memory Authority Model](../proposals/memory-authority-model-proposal.md)
- [Memory Authority Model Backlog](../backlog/memory-authority-model.md)
- `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](../research/zircon.md) grounds the separation between a
  memory object and its per-address-space mappings.
- [Genode](../research/genode.md) grounds explicit, bounded resource donation
  and accounting for shared-memory objects.