Struct NodeOwner 

pub struct NodeOwner<C: PageTableConfig> {
    pub meta_own: PageMetaOwner,
    pub children_perm: PointsTo<C::E, NR_ENTRIES>,
    pub level: PagingLevel,
    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

children_perm: PointsTo<C::E, NR_ENTRIES>

level: PagingLevel

tree_level: int

slot_index: int

Implementations

impl<C: PageTableConfig> NodeOwner<C>

pub open spec fn meta_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],
        regions.slot_owners[self.slot_index].metadata_perm,
        (),
    )
}

pub open spec fn meta_value(self, regions: MetaRegionOwners) -> PageTablePageMeta<C>

{
    typed_meta_value::<
        PageTablePageMeta<C>,
    >(regions.slot_owners[self.slot_index].metadata_perm, ())
}

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

{
    let idx = self.slot_index;
    &&& regions.contains(idx)
    &&& self.meta_wf(regions)
    &&& self.meta_value(regions).wf(self.meta_own)
    &&& self.level == self.meta_value(regions).level
    &&& self.meta_own.nr_children.id() == self.meta_value(regions).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.meta_vaddr()
    &&& guard.inner.inner@.wf(self)

}

Trait Implementations

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

open spec fn inv(self) -> bool

{
    &&& self.meta_own.inv()
    &&& 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()
    &&& self.slot_index == meta_to_index(index_to_meta(self.slot_index))

}

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

proof fn view_preserves_inv(self)

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

open spec fn view(&self) -> <Self as View>::V

{
    NodeModel {
        level: self.level,
        _phantom: core::marker::PhantomData,
    }
}

type V = NodeModel<C>