PageTableNode

ostd::mm::page_table

Type Alias PageTableNode 

Source 
pub type PageTableNode<C> = Frame<PageTablePageMeta<C>>;
Expand description

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§

#[repr(transparent)]
pub struct PageTableNode<C> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<PageTablePageMeta<C>>,
}

Fields§

§ptr: PPtr<MetaSlot>§_marker: PhantomData<PageTablePageMeta<C>>

Implementations§

Source§

impl<C: PageTableConfig> PageTableNode<C>

Source

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<'rcu, C>>,
Ghost(idx): Ghost<usize>,
->
owner: Tracked<OwnerSubtree<C>>,
requires
1 <= level < NR_LEVELS,
idx < NR_ENTRIES,
old(regions).inv(),
old(parent_owner).inv(),
ensures
regions.inv(),
parent_owner.inv(),
allocated_empty_node_owner(owner@, level),
res.ptr.addr() == owner@.value.node.unwrap().meta_perm.addr(),
guards.unlocked(owner@.value.node.unwrap().meta_perm.addr()),
MetaSlot::get_from_unused_spec(
    meta_to_frame(owner@.value.node.unwrap().meta_perm.addr()),
    false,
    *old(regions),
    *regions,
),
owner@.value.relate_region(*regions),
owner@.value.in_scope,
owner@
    .value
    .match_pte(
        C::E::new_pt_spec(meta_to_frame(owner@.value.node.unwrap().meta_perm.addr())),
        level as PagingLevel,
    ),
*parent_owner
    == old(parent_owner)
        .set_children_perm(
            idx,
            C::E::new_pt_spec(meta_to_frame(owner@.value.node.unwrap().meta_perm.addr())),
        ),

Allocates a new empty page table node.

Source§

impl<C: PageTableConfig> PageTableNode<C>

Source

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

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

}

Trait Implementations§

Source§

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

Source§

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

{
    &&& self.ptr.addr() == owner.meta_perm.addr()

}
Source§

type Owner = NodeOwner<C>

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