Skip to main content

PageTablePageMeta

ostd::mm::page_table

Struct PageTablePageMeta 

Source 
pub struct PageTablePageMeta<C: PageTableConfig> {
    pub nr_children: PCell<u16>,
    pub stray: PCell<bool>,
    pub level: PagingLevel,
    pub lock: PAtomicU8,
    pub _phantom: PhantomData<C>,
}
Expand description

The metadata of any kinds of page table pages. Make sure the the generic parameters don’t effect the memory layout.

Fields§

§nr_children: PCell<u16>

The number of valid PTEs. It is mutable if the lock is held.

§stray: PCell<bool>

If the page table is detached from its parent.

A page table can be detached from its parent while still being accessed, since we use a RCU scheme to recycle page tables. If this flag is set, it means that the parent is recycling the page table.

§level: PagingLevel

The level of the page table page. A page table page cannot be referenced by page tables of different levels.

§lock: PAtomicU8

The lock for the page table page.

§_phantom: PhantomData<C>

Implementations§

Source§

impl<C: PageTableConfig> PageTablePageMeta<C>

Source

pub exec fn new(level: PagingLevel) -> Self

Source

pub open spec fn walk_pte_at_view(view: MemView, c: usize) -> C::E

{ ostd_pod::decode_pod::<C::E>(view.read_bytes(c, core::mem::size_of::<C::E>())) }

The PTE value that read_once::<C::E> would produce at cursor c against the given memory view. Linked to read_once via pod_bytes(v) == read_view.read_bytes(...) (strengthened ensures)

  • [lemma_decode_pod_inverse].
Source

pub open spec fn walk_coverage_at(self, view: MemView, dom: Set<usize>, c: usize) -> bool

{
    let pte = Self::walk_pte_at_view(view, c);
    pte.is_present() && !pte.is_last(self.level)
        ==> dom.contains(frame_to_index(pte.paddr()))
}

Single-cursor projection of [walk_coverage_from_view]. Extracting the forall body to a named predicate lets the body invoke [lemma_coverage_at] for one specific c instead of relying on auto-trigger matching across the loop invariant’s forall|c|.

Source

pub proof fn lemma_coverage_at( self, reader: VmReader<'_, Infallible>, view: MemView, dom: Set<usize>, c: usize, )

requires
self.walk_coverage_from_view(reader, view, dom),
reader.cursor.vaddr <= c,
c + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),
(c - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,
ensures
self.walk_coverage_at(view, dom, c),

Instantiate [walk_coverage_from_view]’s forall at one cursor.

Source

pub proof fn lemma_uniqueness_at_pair( self, reader: VmReader<'_, Infallible>, view: MemView, c1: usize, c2: usize, )

requires
self.walk_uniqueness_from_view(reader, view),
reader.cursor.vaddr <= c1,
c1 + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),
(c1 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,
reader.cursor.vaddr <= c2,
c2 + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),
(c2 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,
c1 != c2,
Self::walk_pte_at_view(view, c1).is_present(),
!Self::walk_pte_at_view(view, c1).is_last(self.level),
Self::walk_pte_at_view(view, c2).is_present(),
!Self::walk_pte_at_view(view, c2).is_last(self.level),
ensures
Self::walk_pte_at_view(view, c1).paddr() != Self::walk_pte_at_view(view, c2).paddr(),

Instantiate [walk_uniqueness_from_view]’s forall at one cursor pair.

Source

pub open spec fn walk_coverage_from_view( self, reader: VmReader<'_, Infallible>, view: MemView, dom: Set<usize>, ) -> bool

{
    forall |c: usize| {
        reader.cursor.vaddr <= c
            && c + core::mem::size_of::<C::E>()
                <= reader.cursor.vaddr + reader.remain_spec()
            && (c - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0
            ==> {
                let pte = Self::walk_pte_at_view(view, c);
                pte.is_present() && !pte.is_last(self.level)
                    ==> dom.contains(frame_to_index(pte.paddr()))
            }
    }
}

Caller-side dom-membership obligation: every present non-last PTE position in the walk (over view) has its child-frame index in dom. Phrased over a frozen (view, dom) pair so the body can carry it as a loop invariant against an entry-state snapshot while vm_io_owner advances per iteration.

Source

pub open spec fn walk_uniqueness_from_view( self, reader: VmReader<'_, Infallible>, view: MemView, ) -> bool

{
    forall |c1: usize, c2: usize| {
        reader.cursor.vaddr <= c1
            && c1 + core::mem::size_of::<C::E>()
                <= reader.cursor.vaddr + reader.remain_spec()
            && (c1 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0
            && reader.cursor.vaddr <= c2
            && c2 + core::mem::size_of::<C::E>()
                <= reader.cursor.vaddr + reader.remain_spec()
            && (c2 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0
            && c1 != c2
            ==> {
                let pte1 = Self::walk_pte_at_view(view, c1);
                let pte2 = Self::walk_pte_at_view(view, c2);
                pte1.is_present() && !pte1.is_last(self.level) && pte2.is_present()
                    && !pte2.is_last(self.level) ==> pte1.paddr() != pte2.paddr()
            }
    }
}

Caller-side uniqueness obligation: distinct cursor positions with present non-last PTEs (in view) map to distinct paddrs.

Source

pub open spec fn child_perms_embedding( regions: MetaRegionOwners, excluded: Set<usize>, ) -> bool

{
    forall |paddr: crate::mm::Paddr| {
        regions.slots.dom().contains(frame_to_index(paddr))
            && !excluded.contains(frame_to_index(paddr))
            ==> {
                let idx = frame_to_index(paddr);
                let so = regions.slot_owners[idx];
                &&& <Frame<Self>>::from_raw_requires_safety(regions, paddr)
                &&& so.inner_perms.ref_count.value() > 0
                &&& so.inner_perms.ref_count.value()
                    != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
                &&& so.inner_perms.ref_count.value()
                    <= crate::specs::mm::frame::meta_owners::REF_COUNT_MAX
                &&& so.inner_perms.ref_count.value() == 1
                    ==> {
                        &&& so.inner_perms.storage.is_init()
                        &&& so.inner_perms.in_list.value() == 0
                        &&& so.paths_in_pt.is_empty()

                    }

            }
    }
}

Caller-side shape obligation: every paddr in child_perms.dom() has a slot perm matching the shape from_raw + VerifiedDrop::drop expect (init, alignment, refcount within bounds, last-reference shape when refcount == 1).

Source§

impl<C: PageTableConfig> PageTablePageMeta<C>

Source

pub open spec fn into_spec(self) -> StoredPageTablePageMeta

{
    StoredPageTablePageMeta {
        nr_children: self.nr_children,
        stray: self.stray,
        level: self.level,
        lock: self.lock,
    }
}
Source

pub exec fn into(self) -> res : StoredPageTablePageMeta

ensures
res == self.into_spec(),

Trait Implementations§

Source§

impl<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C>

Source§

open spec fn on_drop_pre( &self, reader: VmReader<'_, Infallible>, regions: MetaRegionOwners, vm_io_owner: VmIoOwner, ) -> bool

{
    &&& reader.inv()
    &&& reader.wf(vm_io_owner)
    &&& reader.remain_spec() >= crate::specs::arch::mm::PAGE_SIZE
    &&& reader.cursor.vaddr % core::mem::align_of::<C::E>() == 0
    &&& vm_io_owner.inv()
    &&& vm_io_owner.read_view_initialized()
    &&& regions.inv()
    &&& Self::child_perms_embedding(regions, vstd::set::Set::empty())
    &&& self
        .walk_coverage_from_view(reader, vm_io_owner.read_view_of(), regions.slots.dom())
    &&& self.walk_uniqueness_from_view(reader, vm_io_owner.read_view_of())

}

Caller invariants the PT-node on_drop body relies on:

  • Reader well-formedness + vm_io_owner matching + read view initialized + at least PAGE_SIZE bytes remaining for the PT-node walk.
  • Global region table invariant.
  • Embedding ([child_perms_embedding]): for every paddr in child_perms.dom(), the slot and perm match from_raw / VerifiedDrop::drop’s expected shape.
  • Walk coverage ([walk_coverage_from_view]): for every present non-last PTE in the page bytes, frame_to_index(pte.paddr()) ∈ child_perms.dom().
  • Walk uniqueness ([walk_uniqueness_from_view]): distinct PTE positions with present non-last PTEs have distinct paddrs.

The body now discharges the dom-membership obligation in full via byte-level chaining (decode_pod + read_once’s strengthened ensures + the byte-preservation loop invariant) plus the two walk-* preconditions; see [lemma_coverage_at] and [lemma_uniqueness_at_pair].

Source§

exec fn on_drop( &mut self, reader: &mut VmReader<'_, Infallible>, verus_tmp_regions: Tracked<&mut MetaRegionOwners>, verus_tmp_vm_io_owner: Tracked<&mut VmIoOwner>, )

Drops the children of a page-table node: walks each present PTE and drops the referenced child page-table-node frame or mapped item.

Source§

exec fn is_untyped(&self) -> bool

Source§

uninterp spec fn vtable_ptr(&self) -> usize

Source§

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

Source§

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

{
    &&& self.nr_children.id() == owner.nr_children.id()
    &&& self.stray.id() == owner.stray.id()
    &&& 0 <= owner.nr_children.value() <= NR_ENTRIES

}
Source§

type Owner = PageMetaOwner

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

impl<C: PageTableConfig> Repr<MetaSlotStorage> for PageTablePageMeta<C>

Source§

open spec fn wf(r: MetaSlotStorage, perm: ()) -> bool

{ matches!(r, MetaSlotStorage::PTNode(_)) }
Source§

open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ())

{ (MetaSlotStorage::PTNode(self.into_spec()), ()) }
Source§

exec fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage

Source§

open spec fn from_repr_spec(r: MetaSlotStorage, perm: ()) -> Self

{
    match r {
        MetaSlotStorage::PTNode(node) => node.into_spec::<C>(),
        _ => arbitrary(),
    }
}
Source§

exec fn from_repr(r: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self

Source§

exec fn from_borrowed<'a>( r: &'a MetaSlotStorage, verus_tmp_perm: Tracked<&'a ()>, ) -> &'a Self

Source§

proof fn from_to_repr(self, perm: ())

Source§

proof fn to_from_repr(r: MetaSlotStorage, perm: ())

Source§

proof fn to_repr_wf(self, perm: ())

Source§

type Perm = ()

If the underlying representation contains cells, the translation may require permission objects that access them.

Auto Trait Implementations§

§

impl<C> !Freeze for PageTablePageMeta<C>

§

impl<C> !RefUnwindSafe for PageTablePageMeta<C>

§

impl<C> Send for PageTablePageMeta<C>

§

impl<C> Sync for PageTablePageMeta<C>

§

impl<C> Unpin for PageTablePageMeta<C>
where C: Unpin,

§

impl<C> UnsafeUnpin for PageTablePageMeta<C>

§

impl<C> UnwindSafe for PageTablePageMeta<C>
where C: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A