pub proof fn vm_space_cursor_embedded<'a, 'rcu>(tracked
vm_space: &VmSpaceOwner,
tracked regions: &mut MetaRegionOwners,
va: Range<Vaddr>,
) -> tracked res : Option<(CursorOwner<'rcu, UserPtConfig>, Guards<'rcu>)>Expand description
requires
vm_space.inv(),old(regions).inv(),final(regions).inv(),final(regions).slots =~= old(regions).slots,forall |i: usize| (
final(regions).slot_owners[i].inner_perms.in_list
== old(regions).slot_owners[i].inner_perms.in_list
),forall |i: usize| (
final(regions).slot_owners[i] != old(regions).slot_owners[i]
==> {
&&& old(regions).slot_owners[i].inner_perms.ref_count.value()
== REF_COUNT_UNUSED
&&& final(regions).slot_owners[i].inner_perms.ref_count.value()
!= REF_COUNT_UNUSED
&&& final(regions).slot_owners[i].usage != PageUsage::Frame
}
),forall |c: CursorOwner<'rcu, UserPtConfig>| {
c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions))
},res matches Some(
(c, g),
) ==> {
&&& c.inv()
&&& c.children_not_locked(g)
&&& c.nodes_locked(g)
&&& !c.popped_too_high
&&& c.metaregion_sound(*final(regions))
},Mirror of crate::mm::vm_space::VmSpace::cursor.
The exec method mutates &mut Guards (adding locks for the new
cursor) and &mut MetaRegionOwners. Here, since each CursorEntry
carries its own self-contained Guards (a per-cursor model
restriction; see module-level docs), we return a fresh Guards
alongside the owner instead of mutating a shared one.
The metaregion_sound_preserves ensures clause says that any
CursorOwner that was sound w.r.t. the old regions is still
sound w.r.t. the new regions. This mirrors the exec
PageTable::cursor ensures that preserves paths_in_pt and
non-saturation across all slots ([page_table/mod.rs:1599-1661]).