PageTableNodeRef

ostd::mm::page_table

Type Alias PageTableNodeRef 

Source 
pub type PageTableNodeRef<'a, C> = FrameRef<'a, PageTablePageMeta<C>>;
Expand description

A reference to a page table node.

Aliased Type§

pub struct PageTableNodeRef<'a, C> {
    pub inner: ManuallyDrop<Frame<PageTablePageMeta<C>>>,
    pub _marker: PhantomData<&'a Frame<PageTablePageMeta<C>>>,
}

Fields§

§inner: ManuallyDrop<Frame<PageTablePageMeta<C>>>§_marker: PhantomData<&'a Frame<PageTablePageMeta<C>>>

Implementations§

Source§

impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C>

Source

pub open spec fn locks_preserved_except<'rcu>( addr: usize, guards0: Guards<'rcu, C>, guards1: Guards<'rcu, C>, ) -> bool

{
    &&& OwnerSubtree::implies(
        CursorOwner::node_unlocked(guards0),
        CursorOwner::node_unlocked_except(guards1, addr),
    )
    &&& forall |i: usize| guards0.lock_held(i) ==> guards1.lock_held(i)
    &&& forall |i: usize| guards0.unlocked(i) && i != addr ==> guards1.unlocked(i)

}
Source

pub exec fn lock<'rcu, A: InAtomicMode>( self, _guard: &'rcu A, ) -> res : PPtr<PageTableGuard<'rcu, C>>
where 'a: 'rcu,

with
Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
->
guard_perm: Tracked<GuardPerm<'rcu, C>>,
requires
self.inner@.invariants(*owner),
old(guards).unlocked(owner.meta_perm.addr()),
ensures
guards.lock_held(owner.meta_perm.addr()),
Self::locks_preserved_except(owner.meta_perm.addr(), *old(guards), *guards),
res.addr() == guard_perm@.addr(),
owner.relate_guard_perm(guard_perm@),

Locks the page table node.

An atomic mode guard is required to

  1. prevent deadlocks;
  2. provide a lifetime ('rcu) that the nodes are guaranteed to outlive.
§Verification Design

As of when we verified this library, we didn’t have a spin lock implementation, so we axiomatize what happens when it’s successful.

Source

pub exec fn make_guard_unchecked<'rcu, A: InAtomicMode>( self, _guard: &'rcu A, ) -> res : PPtr<PageTableGuard<'rcu, C>>
where 'a: 'rcu,

with
Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
->
guard_perm: Tracked<GuardPerm<'rcu, C>>,
requires
self.inner@.invariants(*owner),
old(guards).unlocked(owner.meta_perm.addr()),
ensures
guards.lock_held(owner.meta_perm.addr()),
Self::locks_preserved_except(owner.meta_perm.addr(), *old(guards), *guards),
res.addr() == guard_perm@.addr(),
owner.relate_guard_perm(guard_perm@),

Creates a new PageTableGuard without checking if the page table lock is held.

§Safety

This function must be called if this task logically holds the lock.

Calling this function when a guard is already created is undefined behavior unless that guard was already forgotten.