Struct NodeOwner 

pub struct NodeOwner<C: PageTableConfig> {
    pub meta_own: PageMetaOwner,
    pub frame_permission: FracMetadataPerm,
    pub children_perm: PointsTo<C::E, NR_ENTRIES>,
    pub tree_level: int,
    pub slot_index: int,
}

Verification Design

The owner type for a page table node. It contains:

• meta_own, a PageMetaOwner, which holds the permissions for node-specific metadata fields, nr_children and stray
• children_perm is an array permission for the underlying frame in which the node is allocated, interpreted as an array of NR_ENTRIES page table entries
• slot_index identifies the underlying frame’s index in the metadata region
• Each node is a page table with a level between 1 and 4 (on x86); level tracks the level of this node.
• tree_level is the level field of the ghost_tree::TreeNode that carries this object. Carried here for convenience, though it can be computed from level.

Fields

meta_own: PageMetaOwner

frame_permission: FracMetadataPerm

children_perm: PointsTo<C::E, NR_ENTRIES>

tree_level: int

slot_index: int

Implementations

impl<C: PageTableConfig> NodeOwner<C>

pub proof fn tracked_borrow_frame_metadata_perm( tracked permission: &FracMetadataPerm, ) -> tracked res : &MetadataPerm

ensures

*res == permission.resource(),

pub proof fn tracked_borrow_metadata_perm(tracked &self) -> tracked &MetadataPerm

returns

self.frame_permission.resource(),

pub open spec fn slot_vaddr(self) -> Vaddr

{ index_to_meta(self.slot_index) }

The meta address of this node’s slot, computed from slot_index.

pub open spec fn meta_wf(self, regions: MetaRegionOwners) -> bool

{
    typed_meta_wf::<
        PageTablePageMeta<C>,
    >(*regions.slots[self.slot_index], self.frame_permission.resource(), ())
}

pub open spec fn meta_value(self) -> PageTablePageMeta<C>

{ typed_meta_value::<PageTablePageMeta<C>>(self.frame_permission.resource(), ()) }

pub open spec fn level(self) -> PagingLevel

{ self.meta_value().level }

pub open spec fn metaregion_sound_node(self, regions: MetaRegionOwners) -> bool

{
    let idx = self.slot_index;
    &&& regions.contains(idx)
    &&& self.frame_permission.id() == regions.slot_owners[idx].metadata_perm.id()
    &&& self.meta_wf(regions)
    &&& self.meta_value().wf(self.meta_own)
    &&& self.meta_own.nr_children.id() == self.meta_value().nr_children.id()
    &&& regions.slot_owners[self.slot_index].usage is PageTable
    &&& self.count_consistent()

}

Regions-tied invariants that used to live in NodeOwner::inv() via the now-removed meta_perm field. Establishes the bridge between the NodeOwner and the slot perm parked in regions.

pub open spec fn count_consistent(self) -> bool

{ self.meta_own.nr_children.value() == count_present(self.children_perm.value()) }

nr_children equals the number of present PTEs in children_perm. Held by a settled node (see metaregion_sound_node’s use site).

impl<C: PageTableConfig> NodeOwner<C>

pub proof fn nr_children_absent_slot_bound(self, idx: usize)

requires

self.inv(),

self.count_consistent(),

self.children_perm.value().len() == NR_ENTRIES,

idx < NR_ENTRIES,

!self.children_perm.value()[idx as int].is_present(),

ensures

self.meta_own.nr_children.value() < NR_ENTRIES,

If a slot in children_perm holds a non-present PTE, then nr_children < NR_ENTRIES. Proven (no longer axiomatized) from the count_consistent invariant: nr_children counts present PTEs, and an absent slot means not all NR_ENTRIES slots are present.

pub proof fn nr_children_present_slot_bound(self, idx: usize)

requires

self.inv(),

self.count_consistent(),

self.children_perm.value().len() == NR_ENTRIES,

idx < NR_ENTRIES,

self.children_perm.value()[idx as int].is_present(),

ensures

self.meta_own.nr_children.value() > 0,

If a slot in children_perm holds a present PTE, then nr_children > 0. Dual of Self::nr_children_absent_slot_bound; proven from count_consistent.

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

pub open spec fn relate_guard(self, guard: PageTableGuard<'rcu, C>) -> bool

{
    &&& guard.inner.inner@.ptr.addr() == self.slot_vaddr()
    &&& guard.inner.inner@.wf(self)
    &&& guard.inner.inner@.external_meta_wf(self.frame_permission.resource(), ())

}

Trait Implementations

impl<C: PageTableConfig> Inv for NodeOwner<C>

open spec fn inv(self) -> bool

{
    &&& self.meta_own.inv()
    &&& self.frame_permission.frac() == 1
    &&& 0 <= self.meta_own.nr_children.value() <= NR_ENTRIES
    &&& 1 <= self.level() <= NR_LEVELS
    &&& self.children_perm.wf()
    &&& self.children_perm.is_init_all()
    &&& self.children_perm.addr()
        == paddr_to_vaddr(meta_to_frame(index_to_meta(self.slot_index)))
    &&& self.tree_level == INC_LEVELS - self.level() - 1
    &&& 0 <= self.slot_index < max_meta_slots()
    &&& FRAME_METADATA_RANGE.start <= index_to_meta(self.slot_index)
        < FRAME_METADATA_RANGE.end
    &&& index_to_meta(self.slot_index) % META_SLOT_SIZE == 0
    &&& meta_to_frame(index_to_meta(self.slot_index))
        < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR
    &&& meta_to_frame(index_to_meta(self.slot_index)) < MAX_PADDR
    &&& meta_to_frame(index_to_meta(self.slot_index)) == self.children_perm.addr()

}