Skip to main content

subtree_unlock_upgrade

ostd::specs::mm::page_table::cursor::cursor_steps

Function subtree_unlock_upgrade 

Source 
pub proof fn subtree_unlock_upgrade<'rcu, C: PageTableConfig>(
    subtree: OwnerSubtree<C>,
    path: TreePath<NR_ENTRIES>,
    guards: Guards<'rcu, C>,
    regions: MetaRegionOwners,
    excepted_addr: usize,
    excepted_path: TreePath<NR_ENTRIES>,
)
Expand description
requires
subtree.inv(),
PageTableOwner::<C>(subtree).pt_inv(),
subtree.tree_predicate_map(path, PageTableOwner::<C>::metaregion_sound_pred(regions)),
subtree
    .tree_predicate_map(
        path,
        CursorOwner::<'rcu, C>::node_unlocked_except(guards, excepted_addr),
    ),
regions.slot_owners[frame_to_index(meta_to_frame(excepted_addr))].paths_in_pt
    == set![excepted_path],
path == subtree.value.path,
path.inv(),
path != excepted_path,
excepted_path.len() <= path.len()
    || (exists |k: int| {
        0 <= k < path.len() && #[trigger] excepted_path.index(k) != path.index(k)
    }),
ensures
subtree.tree_predicate_map(path, CursorOwner::<'rcu, C>::node_unlocked(guards)),

Upgrade node_unlocked_except to node_unlocked on a subtree where the excepted entry cannot appear. The precondition path == subtree.value.path ties structural positions to entry paths. excepted_path must differ from all descendant paths, which is guaranteed when excepted_path != path and excepted_path is not an extension of path (all descendants have paths extending path).