Skip to main content

Module unique

ostd::specs::mm::embedding

Module unique 

Source
Expand description

Embedding of UniqueFrame lifecycle operations: allocate (unique_from_unused_embedded) and drop (unique_drop_embedded).

A UniqueFrame handle in the embedding is a paddr-bearing super::UniqueEntry in super::VmStore::unique_frames. Unlike a shared super::FrameEntry, a unique handle drives its slot’s ref_count to the REF_COUNT_UNIQUE sentinel (u64::MAX - 1), which is not a participant in the rc == H + P + cover_count accounting equation. Exclusivity (rc == REF_COUNT_UNIQUE ⟹ no shared users: handle_count == 0, paths_in_pt empty, segment_cover_count == 0) needs no dedicated invariant clause: it is implied by the equation itself — a user at a usage == Frame slot fires the equation’s antecedent and demands rc != UNIQUE, contradicting rc == UNIQUE. So unique_drop_embedded’s caller recovers the “no users” facts by deriving that contradiction.

§Methods modeled

  • UniqueFrame::from_unused: allocate a fresh exclusive handle on a previously-unused slot. The slot transitions usage == Unused, rc == UNUSED → usage == Frame, rc == UNIQUE.
  • UniqueFrame drop: tear down the exclusive handle. The slot transitions rc == UNIQUE → rc == UNUSED (last-ref teardown, uninitialising storage), with usage / paths_in_pt (empty) / in_list preserved — the same shape as Frame’s last-ref teardown.
  • Frame::from_unique (from_unique_embedded): convert the exclusive handle to a shared one — rc drops UNIQUE → 1, consuming the super::UniqueEntry and minting a super::FrameEntry (H: 0 → 1).
  • UniqueFrame::try_from_shared (try_from_shared_embedded): convert a sole-reference shared handle (rc == 1) back to an exclusive one — rc rises 1 → UNIQUE, consuming the FrameEntry and minting a UniqueEntry. Fallible: if the slot is not the sole reference (rc != 1) the CAS fails and the step is a no-op (the shared handle is returned unchanged).

§Model gaps

  • into_raw / from_raw (pub(crate)-only) and the accessors (meta / meta_mut / repurpose / transmute / start_paddr): no embedding state change / not surfaced.

Functions§

from_unique_embedded
try_from_shared_embedded
unique_drop_embedded
unique_from_unused_embedded