Struct Entry 

pub struct Entry<'a, 'rcu, C: PageTableConfig> {
    pub pte: C::E,
    pub idx: usize,
    pub node: &'a mut PageTableGuard<'rcu, C>,
}

Fields

pte: C::E

The page table entry.

We store the page table entry here to optimize the number of reads from the node. We cannot hold a &mut E reference to the entry because that other CPUs may modify the memory location for accessed/dirty bits. Such accesses will violate the aliasing rules of Rust and cause undefined behaviors.

Verification Design

The concrete value of a PTE is specific to the architecture and the page table configuration, represented by the type C::E. We represent its value as an abstract EntryOwner, which is connected to the concrete value by match_pte. The EntryOwner is well-formed with respect to Entry if it is related to the concrete value by match_pte.

An Entry can be thought of as a mutable handle to the concrete value of the PTE. The node field is a mutable reference to the guard of the node that contains the entry, index provides the offset, and the pte is current value. Only one Entry can exist for a given node at any given time.

idx: usize

The index of the entry in the node.

node: &'a mut PageTableGuard<'rcu, C>

The node that contains the entry.

Implementations

impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C>

pub open spec fn new_spec( pte: C::E, idx: usize, node: &'a mut PageTableGuard<'rcu, C>, ) -> Self

{ Self { pte, idx, node } }

pub exec fn new(pte: C::E, idx: usize, node: &'a mut PageTableGuard<'rcu, C>) -> res : Self

ensures

res.pte == pte,

res.idx == idx,

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

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

impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C>

pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool

{
    &&& owner.inv()
    &&& regions.inv()
    &&& self.wf(owner)
    &&& owner.metaregion_sound(regions)

}

pub open spec fn node_matching( self, owner: EntryOwner<C>, parent_owner: NodeOwner<C>, guard: PageTableGuard<'rcu, C>, ) -> bool

{
    &&& parent_owner.level() == owner.parent_level
    &&& parent_owner.inv()
    &&& parent_owner.relate_guard(guard)
    &&& owner
        .match_pte(
            parent_owner.children_perm.value()[self.idx as int],
            owner.parent_level,
        )

}

pub open spec fn metaregion_sound_preserved( regions0: MetaRegionOwners, regions1: MetaRegionOwners, ) -> bool

{
    OwnerSubtree::implies(
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
            entry.metaregion_sound(regions0)
        },
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
            entry.metaregion_sound(regions1)
        },
    )
}

pub open spec fn replace_nonpanic_condition( parent_owner: NodeOwner<C>, new_owner: EntryOwner<C>, ) -> bool

{
    if new_owner.is_node() {
        parent_owner.level() - 1 == new_owner.node().level()
    } else if new_owner.is_frame() {
        parent_owner.level() == new_owner.parent_level
    } else {
        true
    }
}

pub open spec fn metaregion_sound_neq_preserved( old_entry_owner: EntryOwner<C>, new_entry_owner: EntryOwner<C>, regions0: MetaRegionOwners, regions1: MetaRegionOwners, ) -> bool

{
    OwnerSubtree::implies(
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
            entry.meta_slot_paddr_neq(old_entry_owner)
                && entry.meta_slot_paddr_neq(new_entry_owner)
                && entry.metaregion_sound(regions0)
        },
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
            entry.metaregion_sound(regions1)
        },
    )
}

pub open spec fn metaregion_sound_neq_old_preserved( old_entry_owner: EntryOwner<C>, regions0: MetaRegionOwners, regions1: MetaRegionOwners, ) -> bool

{
    OwnerSubtree::implies(
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
            entry.meta_slot_paddr_neq(old_entry_owner)
                && entry.metaregion_sound(regions0)
        },
        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
            entry.metaregion_sound(regions1)
        },
    )
}

When the new child is NOT a node, into_pte doesn’t modify raw_count. Only paths_in_pt changes at new_idx, which metaregion_sound doesn’t inspect. So entries with paddr_neq(old_child) preserve metaregion_sound — no paddr_neq(new_child) needed.

pub proof fn alloc_if_none_metaregion_sound_preserved( old_child: EntryOwner<C>, new_child: EntryOwner<C>, regions0: MetaRegionOwners, regions1: MetaRegionOwners, )

requires

old_child.is_absent(),

old_child.inv(),

new_child.is_node(),

regions0.inv(),

regions0.contains(frame_to_index(new_child.meta_slot_paddr()->0)),

regions0.slot_owner(new_child.meta_slot_paddr()->0).ref_count() == REF_COUNT_UNUSED,

!crate::specs::mm::frame::meta_owners::is_mmio_paddr(new_child.meta_slot_paddr()->0),

Self::metaregion_sound_neq_preserved(old_child, new_child, regions0, regions1),

ensures

Self::metaregion_sound_preserved(regions0, regions1),

When alloc_if_none allocates a new node from an absent slot, all existing entries’ metaregion_sound is preserved in the new regions.

Justification: metaregion_sound_neq_preserved gives preservation for entries whose paddr differs from both old_child and new_child. Old_child is absent (paddr_neq trivially true).

pub open spec fn path_tracked_pred_preserved( regions0: MetaRegionOwners, regions1: MetaRegionOwners, ) -> bool

{
    OwnerSubtree::implies(
        PageTableOwner::<C>::path_tracked_pred(regions0),
        PageTableOwner::<C>::path_tracked_pred(regions1),
    )
}

pub open spec fn new_owner_compatible( self, new_child: Child<C>, old_owner: EntryOwner<C>, new_owner: EntryOwner<C>, regions: MetaRegionOwners, ) -> bool

{
    &&& old_owner.path == new_owner.path
    &&& old_owner.parent_level == new_owner.parent_level
    &&& new_owner.is_node()
        ==> {
            &&& regions.contains(frame_to_index(new_owner.meta_slot_paddr()->0))
            &&& regions.slot_owner(new_owner.meta_slot_paddr()->0).ref_count()
                != REF_COUNT_UNUSED

        }

}

pub open spec fn parent_perms_preserved( self, parent_owner0: NodeOwner<C>, parent_owner1: NodeOwner<C>, ) -> bool

{
    &&& forall |i: int| {
        0 <= i < NR_ENTRIES
            ==> (i != self.idx
                ==> parent_owner0.children_perm.value()[i]
                    == parent_owner1.children_perm.value()[i])
    }
    &&& parent_owner1.slot_index == parent_owner0.slot_index
    &&& parent_owner1.level() == parent_owner0.level()
    &&& parent_owner1.tree_level == parent_owner0.tree_level
    &&& parent_owner1.meta_own.nr_children.id()
        == parent_owner0.meta_own.nr_children.id()
    &&& parent_owner1.meta_own.stray == parent_owner0.meta_own.stray

}

Trait Implementations

impl<'a, 'rcu, C: PageTableConfig> OwnerOf for Entry<'a, 'rcu, C>

open spec fn wf(self, owner: Self::Owner) -> bool

{
    &&& self.idx < NR_ENTRIES
    &&& owner.match_pte(self.pte, owner.parent_level)
    &&& valid_frame_paddr(self.pte.paddr())

}

type Owner = EntryOwner<C>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.