Skip to main content

cursor_query_embedded

ostd::specs::mm::embedding::cursor

Function cursor_query_embedded 

Source 
pub proof fn cursor_query_embedded<'rcu>(tracked 
    owner: &mut CursorOwner<'rcu, UserPtConfig>,
tracked     regions: &mut MetaRegionOwners,
tracked     guards: &mut Guards<'rcu>,
) -> res : Option<Paddr>
Expand description
requires
old(owner).inv(),
old(regions).inv(),
old(owner).children_not_locked(*old(guards)),
old(owner).nodes_locked(*old(guards)),
old(owner).metaregion_sound(*old(regions)),
!old(owner).popped_too_high,
ensures
final(owner).inv(),
final(regions).inv(),
final(owner).children_not_locked(*final(guards)),
final(owner).nodes_locked(*final(guards)),
final(owner).metaregion_sound(*final(regions)),
!final(owner).popped_too_high,
final(regions).slots =~= old(regions).slots,
res is None
    ==> forall |i: usize| final(regions).slot_owners[i] == old(regions).slot_owners[i],
res matches Some(
    paddr,
) ==> {
    &&& has_safe_slot(paddr)
    &&& old(regions).slot_owners[frame_to_index(paddr)].usage == PageUsage::Frame
    &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
        == (old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
            + 1) as nat
    &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
        <= REF_COUNT_MAX
    &&& forall |i: usize| {
        i != frame_to_index(paddr)
            ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
    }
    &&& final(regions).slot_owners[frame_to_index(paddr)].self_addr
        == old(regions).slot_owners[frame_to_index(paddr)].self_addr
    &&& final(regions).slot_owners[frame_to_index(paddr)].usage
        == old(regions).slot_owners[frame_to_index(paddr)].usage
    &&& final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt
        == old(regions).slot_owners[frame_to_index(paddr)].paths_in_pt
    &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list
        == old(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list
    &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage
        == old(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage
    &&& final(regions).slot_owners[frame_to_index(paddr)].inner_perms.vtable_ptr
        == old(regions).slot_owners[frame_to_index(paddr)].inner_perms.vtable_ptr

},
forall |c: CursorOwner<'rcu, UserPtConfig>| {
    c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},

Mirror of crate::mm::vm_space::Cursor::query / crate::mm::vm_space::CursorMut::query.

Exec requires invariants(owner, regions, guards). It does not require owner.in_locked_range(): an out-of-range cursor is handled by Cursor::query’s graceful Err (the exec requires was relaxed accordingly; in_locked_range now only governs success, not safety).

metaregion_sound_preserves: a CursorOwner that was sound w.r.t. the old regions is still sound w.r.t. the new regions. This keeps VmStore::inv chainable across method calls that touch regions.

Result Some(paddr) / None. Exec query returns (Range<Vaddr>, Option<MappedItem>). When the inner Option is Some(item) and the item is tracked (non-MMIO), exec clone_item bumps rc at the leaf slot by one. The returned Paddr here is the cloned leaf’s physical address (i.e. the new handle the caller now logically owns); the embedding’s [step_query] registers a fresh [FrameEntry] at that paddr to keep accounting_inv’s rc == H + P chained. None covers three cases: query returned Err (out of range), query returned Ok(_, None) (cursor not at a leaf), or query returned a Some non-tracked (MMIO) item (clone_item is a no-op for those). In all three None subcases slot_owners is fully preserved.