Struct PageTableGuard 

pub struct PageTableGuard<'rcu, C: PageTableConfig> {
    pub inner: PageTableNodeRef<'rcu, C>,
}

A guard that holds the lock of a page table node.

Fields

inner: PageTableNodeRef<'rcu, C>

Implementations

impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C>

pub exec fn entry<'a>(&'a mut self, idx: usize) -> res : Entry<'a, 'rcu, C>

with

Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(child_owner): Tracked<&EntryOwner<C>>,
Tracked(regions): Tracked<&MetaRegionOwners>,

requires

owner.inv(),

child_owner.inv(),

owner.relate_guard(*old(self)),

child_owner.match_pte(owner.children_perm.value()[idx as int], child_owner.parent_level),

regions.inv(),

regions.contains(owner.slot_index),

idx < NR_ENTRIES,

ensures

res.wf(*child_owner),

res.idx == idx,

*res.node == *old(self),

*final(self) == *final(res.node),

owner.relate_guard(*res.node),

Borrows an entry in the node at a given index.

Panics

Panics if the index is not within the bound of nr_subpage_per_huge<C>.

pub exec fn nr_children(&self) -> nr : u16

with

Tracked(owner): Tracked<&NodeOwner<C>>,

requires

owner.meta_own.nr_children.id() == owner.meta_value().nr_children.id(),

self.inner.inner@.invariants(*owner),

self.inner.inner@.external_meta_wf(owner.frame_permission.resource(), ()),

returns

owner.meta_own.nr_children.value(),

Gets the number of valid PTEs in a page table node.

Verified Properties

Preconditions

• The node must be well-formed.

Postconditions

• Returns the number of valid PTEs in the node.

Safety

• We require the caller to provide a permission token to ensure that this function is only called on a valid page table node.

pub unsafe exec fn read_pte(&self, idx: usize) -> pte : C::E

with

Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(regions): Tracked<&MetaRegionOwners>,

requires

self.inner.inner@.invariants(*owner),

regions.inv(),

regions.contains(owner.slot_index),

idx < NR_ENTRIES,

ensures

pte == owner.children_perm.value()[idx as int],

Reads a non-owning PTE at the given index.

A non-owning PTE means that it does not account for a reference count of the a page if the PTE points to a page. The original PTE still owns the child page.

Safety

The caller must ensure that the index is within the bound.

pub unsafe exec fn write_pte(&mut self, idx: usize, pte: C::E)

with

Tracked(owner): Tracked<&mut NodeOwner<C>>,
Tracked(regions): Tracked<&MetaRegionOwners>,

requires

old(self).inner.inner@.invariants(*old(owner)),

regions.inv(),

regions.contains(old(owner).slot_index),

idx < NR_ENTRIES,

ensures

final(owner).inv(),

final(owner).level() == old(owner).level(),

final(owner).meta_own == old(owner).meta_own,

final(owner).frame_permission == old(owner).frame_permission,

final(owner).slot_index == old(owner).slot_index,

final(owner).children_perm.value()
    == old(owner).children_perm.value().update(idx as int, pte),

*final(self) == *old(self),

Writes a page table entry at a given index.

This operation will leak the old child if the old PTE is present.

Safety

The caller must ensure that:

1. The index must be within the bound;
2. The PTE must represent a valid Child whose level is compatible with the page table node.
3. The page table node will have the ownership of the Child after this method.

Methods from Deref<Target = Frame<M>>

pub exec fn meta<'a>(&'a self) -> ret : &'a M

with

Tracked(metadata_perm): Tracked<Option<&'a MetadataPerm>>,
Tracked(repr_perm): Tracked<&'a M::ReprPerm>,

requires

self.ptr_inv(),

{
    self.inv() && metadata_perm is None
        && typed_meta_wf::<M>(self.slot_perm(), self.metadata_perm(), *repr_perm)
        || metadata_perm is Some && self.external_meta_wf(*metadata_perm->0, *repr_perm)
},

ensures

{
    let metadata_perm = if metadata_perm is Some {
        *metadata_perm->0
    } else {
        self.metadata_perm()
    };
    ret == typed_meta_value::<M>(metadata_perm, *repr_perm)
},

Gets the metadata of this page.

Verified Properties

Preconditions

• The caller must have a valid permission for the frame.

Postconditions

• The function returns the borrowed metadata of the frame.

Safety

• By requiring the caller to provide a typed permission, we ensure that the metadata is of type M. While a non-verified caller cannot be trusted to obey this interface, all functions that return a Frame<M> also return an appropriate permission.

pub exec fn start_paddr(&self) -> Paddr

requires

self.ptr_inv(),

returns

self.start_paddr_spec(),

Gets the physical address of the start of the frame.

Verified Properties

Preconditions

• Bookkeeping: takes the permission for the frame’s metadata slot.

Postconditions

• Correctness: returns the physical address of the frame.

Safety

The caller cannot obtain a frame that doesn’t have a valid permission, and this function does not mutate any state, so it is always sound to call.

pub exec fn map_level(&self) -> PagingLevel

returns

1u8,

Gets the map level of this page.

This is the level of the page table entry that maps the frame, which determines the size of the frame.

Currently, the level is always 1, which means the frame is a regular page frame.

pub exec fn size(&self) -> usize

returns

PAGE_SIZE,

Gets the size of this page in bytes.

pub exec fn reference_count(&self) -> u64

with

Tracked(slot_own): Tracked<&MetaSlotOwner>,

requires

self.ptr_inv(),

self.tracked_slot_perm@.value().wf(*slot_own),

returns

slot_own.ref_count(),

Gets the reference count of the frame.

It returns the number of all references to the frame, including all the existing frame handles (Frame, Frame<dyn AnyFrameMeta>), and all the mappings in the page table that points to the frame.

Safety

The function is safe to call, but using it requires extra care. The reference count can be changed by other threads at any time including potentially between calling this method and acting on the result.

Verified Properties

Preconditions

• Safety Invariant: Metaslot region invariants must hold.
• Bookkeeping: The caller must have a valid and well-typed permission for the frame.

Postconditions

• Correctness: The function returns the reference count of the frame.

pub exec fn borrow<'a>(&self) -> res : FrameRef<'a, M>

requires

self.inv(),

ensures

res.inner@.ptr.addr() == self.ptr.addr(),

Borrows a reference from the given frame.

Verified Properties

Preconditions

• Safety Invariant: Metaslot region invariants must hold.

Postconditions

• Safety Invariant: Metaslot region invariants hold after the call.
• Correctness: The function returns a reference to the frame.
• Correctness: The system context is unchanged.

pub exec fn slot<'a>(&'a self) -> &'a MetaSlot

requires

self.ptr_inv(),

returns

self.tracked_slot_perm@.value(),

Gets the metadata slot of the frame.

Verified Properties

Preconditions

• Safety: The caller must have a valid permission for the frame.

Postconditions

• Correctness: The function returns a reference to the metadata slot of the frame.

Safety

• There is no way to mutably borrow the metadata slot, so taking an immutable reference is safe. (The fields of the slot can be mutably borrowed, but not the slot itself.)

Trait Implementations

impl<'rcu, C: PageTableConfig> Deref for PageTableGuard<'rcu, C>

exec fn deref(&self) -> &Self::Target

returns

self.inner,

type Target = FrameRef<'rcu, PageTablePageMeta<C>>

The resulting type after dereferencing.

impl<'rcu, C: PageTableConfig> TrackDrop for PageTableGuard<'rcu, C>

type Obligation = DropObligation<usize>

The node address whose lock this guard holds. The token thus identifies which guard it tracks; drop_requires’s key match prevents a guard’s obligation from being used to drop a different guard. The real lock-set ledger is Guards::guards; this trait’s discipline lifts the existing state-side discipline onto the obligation token by carrying the locked address.

open spec fn tracked_redeem_requires(self, s: Self::State) -> bool

{ s.lock_held(self.inner.inner@.ptr.addr()) }

open spec fn tracked_redeem_ensures( self, s0: Self::State, s1: Self::State, obl: Self::Obligation, ) -> bool

{
    &&& s1.guards == s0.guards.remove(self.inner.inner@.ptr.addr())
    &&& obl.value() == self.inner.inner@.ptr.addr()

}

proof fn tracked_redeem(self, tracked s: &mut Self::State) -> tracked obl : Self::Obligation

open spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool

{
    &&& s.unlocked(self.inner.inner@.ptr.addr())
    &&& obl.value() == self.inner.inner@.ptr.addr()

}

open spec fn drop_ensures( self, s0: Self::State, s1: Self::State, obl: Self::Obligation, ) -> bool

{ s1.guards == s0.guards.insert(self.inner.inner@.ptr.addr()) }

type State = Guards

A ghost state that originally holds the authoritative drop permission.