Type Alias PageTableNode 

pub type PageTableNode<C> = Frame<PageTablePageMeta<C>>;

A smart pointer to a page table node.

This smart pointer is an owner of a page table node. Thus creating and dropping it will affect the reference count of the page table node. If dropped it as the last reference, the page table node and subsequent children will be freed.

PageTableNode is read-only. To modify the page table node, lock and use PageTableGuard.

Aliased Type

pub struct PageTableNode<C> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<PageTablePageMeta<C>>,
    pub tracked_slot_perm: Tracked<&'static PointsTo<MetaSlot>>,
    pub tracked_metadata_perm: Tracked<Option<Count<MetadataPerm, 9223372036854775807>>>,
}

Fields

ptr: PPtr<MetaSlot>

_marker: PhantomData<PageTablePageMeta<C>>

tracked_slot_perm: Tracked<&'static PointsTo<MetaSlot>>

The permission to access the MetaSlot fields.

tracked_metadata_perm: Tracked<Option<Count<MetadataPerm, 9223372036854775807>>>

One fractional permission for the currently installed metadata.

Implementations

impl<C: PageTableConfig> PageTableNode<C>

pub exec fn alloc<'rcu>(level: PagingLevel) -> res : Self

with

Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&Guards>,
Ghost(idx): Ghost<usize>,
->
owner: Tracked<OwnerSubtree<C>>,

requires

1 <= level < NR_LEVELS,

idx < NR_ENTRIES,

old(regions).inv(),

old(parent_owner).inv(),

ensures

final(regions).inv(),

final(parent_owner).inv(),

allocated_empty_node_owner(owner@, level),

allocated_empty_node_grandchildren_none(owner@),

res.ptr.addr() == owner@.value().node().slot_vaddr(),

res.inv(),

res.wf_with_region(*final(regions)),

guards.unlocked(owner@.value().node().slot_vaddr()),

MetaSlot::get_node_from_unused_spec(
    meta_to_frame(owner@.value().node().slot_vaddr()),
    *old(regions),
    *final(regions),
),

MetaSlot::slot_perm_reparked_spec(
    meta_to_frame(owner@.value().node().slot_vaddr()),
    *old(regions),
    *final(regions),
),

old(regions).contains(meta_to_index(owner@.value().node().slot_vaddr())),

!crate::specs::mm::frame::meta_owners::is_mmio_paddr(
    meta_to_frame(owner@.value().node().slot_vaddr()),
),

owner@.value().metaregion_sound(*final(regions)),

forall |i: int| {
    #[trigger] old(regions).ref_count(i) != REF_COUNT_UNUSED
        ==> i != meta_to_index(owner@.value().node().slot_vaddr())
},

owner@
    .value()
    .match_pte(
        C::E::new_pt_spec(meta_to_frame(owner@.value().node().slot_vaddr())),
        level as PagingLevel,
    ),

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

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

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

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

final(parent_owner).tree_level == old(parent_owner).tree_level,

final(parent_owner).children_perm.addr() == old(parent_owner).children_perm.addr(),

final(parent_owner).children_perm.value()
    == old(parent_owner)
        .children_perm
        .value()
        .update(
            idx as int,
            C::E::new_pt_spec(meta_to_frame(owner@.value().node().slot_vaddr())),
        ),

final(regions).contains(owner@.value().node().slot_index),

owner@.value().node().metaregion_sound_node(*final(regions)),

Allocates a new empty page table node.

impl<C: PageTableConfig> PageTableNode<C>

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

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

}

Trait Implementations

impl<C: PageTableConfig> OwnerOf for PageTableNode<C>

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

{
    &&& self.ptr.addr() == owner.slot_vaddr()
    &&& self.ptr_inv()

}

type Owner = NodeOwner<C>

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