PageTableNodeRef

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: NeverDrop<Frame<PageTablePageMeta<C>>>,
    pub _marker: PhantomData<&'a Frame<PageTablePageMeta<C>>>,
}

Fields§

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

Implementations§

Source§

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

Source

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

with
Tracked(guards): Tracked <& mut Guards <'rcu,C>>,
->
guard_perm: Tracked <GuardPerm <'rcu,C>>,

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.
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
owner.inv(),
self.inner@.wf(*owner),
!old(guards).guards.contains_key(owner.meta_perm.addr()),
old(guards).unlocked(owner.meta_perm.addr()),
ensures
guards.lock_held(owner.meta_perm.addr()),
OwnerSubtree::implies(
    CursorOwner::node_unlocked(*old(guards)),
    CursorOwner::node_unlocked_except(*guards, owner.meta_perm.addr()),
),
forall |i: usize| old(guards).lock_held(i) ==> guards.lock_held(i),
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.