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

Function cursor_mut_unmap_embedded

pub proof fn cursor_mut_unmap_embedded<'rcu>(tracked 
    owner: &mut CursorOwner<'rcu, UserPtConfig>,
tracked     regions: &mut MetaRegionOwners,
tracked     guards: &mut Guards<'rcu>,
tracked     tlb_model: &mut TlbModel,
    len: usize,
)

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,

old(tlb_model).inv(),

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(tlb_model).inv(),

final(regions).slots =~= old(regions).slots,

forall |i: usize| {
    &&& final(regions).slot_owners[i].self_addr == old(regions).slot_owners[i].self_addr
    &&& final(regions).slot_owners[i].usage == old(regions).slot_owners[i].usage
    &&& final(regions).slot_owners[i].inner_perms.in_list
        == old(regions).slot_owners[i].inner_perms.in_list
    &&& final(regions).slot_owners[i].inner_perms.vtable_ptr
        == old(regions).slot_owners[i].inner_perms.vtable_ptr
    &&& old(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNIQUE
        ==> final(regions).slot_owners[i].inner_perms.ref_count.value()
            != REF_COUNT_UNIQUE
    &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
        ==> final(regions).slot_owners[i].inner_perms.storage
            == old(regions).slot_owners[i].inner_perms.storage

},

forall |i: usize| {
    old(regions).slot_owners[i].usage == PageUsage::Frame
        ==> {
            &&& final(regions).slot_owners[i].inner_perms.ref_count.value()
                + old(regions).slot_owners[i].paths_in_pt.len()
                == old(regions).slot_owners[i].inner_perms.ref_count.value()
                    + final(regions).slot_owners[i].paths_in_pt.len()
            &&& final(regions).slot_owners[i].inner_perms.ref_count.value()
                <= old(regions).slot_owners[i].inner_perms.ref_count.value()
            &&& final(regions).slot_owners[i].paths_in_pt.len()
                <= old(regions).slot_owners[i].paths_in_pt.len()
            &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != 0

        }
},

forall |i: usize| {
    old(regions).slot_owners[i].usage == PageUsage::MMIO
        ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
},

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

Mirror of crate::mm::vm_space::CursorMut::unmap.

Exec requires (line 865-866):

invariants(cursor_owner, regions, guards)
tlb_model.inv()

Does NOT require in_locked_range() (the method walks len bytes from the cursor, advancing into the locked range as needed).

cursor_mut_unmap_embedded

Function cursor_mut_unmap_embedded Copy item path

Function cursor_mut_unmap_embedded