Skip to main content

frame_from_unused_embedded

ostd::specs::mm::embedding::frame

Function frame_from_unused_embedded 

Source 
pub proof fn frame_from_unused_embedded(tracked 
    regions: &mut MetaRegionOwners,
    paddr: Paddr,
) -> tracked res : Option<()>
Expand description
requires
old(regions).inv(),
has_safe_slot(paddr) ==> old(regions).slots.contains_key(frame_to_index(paddr)),
ensures
final(regions).inv(),
!has_safe_slot(paddr) ==> res is None,
res is Some
    ==> MetaSlot::get_from_unused_spec(paddr, false, *old(regions), *final(regions)),
res is Some ==> MetaSlot::slot_perm_reparked_spec(paddr, *old(regions), *final(regions)),
res is None ==> *final(regions) == *old(regions),
forall |c: CursorOwner<'_, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::frame::Frame::from_unused (non-unique branch: as_unique = false) including the Design-B caller re-park. On Some, the slot at paddr transitions from REF_COUNT_UNUSED to 1, with usage == Frame and paths_in_pt preserved, and the slot perm is re-parked into regions.slots (domain preserved — see MetaSlot::slot_perm_reparked_spec). The embedding is the caller of Frame::from_unused, and its FrameEntry does not carry the perm, so the modeled atomic step is “allocate + re-park”.

metaregion_sound-preserves: any CursorOwner sound w.r.t. the old regions is still sound w.r.t. the new regions. This is because the only slot whose state changes is at paddr, which must have been UNUSED before (and any sound cursor’s paths_in_pt can only reference non-UNUSED slots).