PageTableGuard

ostd::mm::page_table

Struct PageTableGuard 

Source 
pub struct PageTableGuard<'rcu, C: PageTableConfig> {
    pub inner: PageTableNodeRef<'rcu, C>,
}
Expand description

A guard that holds the lock of a page table node.

Fields§

§inner: PageTableNodeRef<'rcu, C>

Implementations§

Source§

impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C>

Source

pub exec fn entry(guard: PPtr<Self>, idx: usize) -> res : Entry<'rcu, C>

with
Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(child_owner): Tracked<&EntryOwner<C>>,
Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>,
requires
owner.inv(),
!child_owner.in_scope,
child_owner.inv(),
owner.relate_guard_perm(*guard_perm),
guard_perm.addr() == guard.addr(),
child_owner.match_pte(owner.children_perm.value()[idx as int], child_owner.parent_level),
idx < NR_ENTRIES,
ensures
res.wf(*child_owner),
res.node.addr() == guard_perm.addr(),
res.idx == idx,

Borrows an entry in the node at a given index.

§Panics

Panics if the index is not within the bound of nr_subpage_per_huge<C>.

Source

pub exec fn nr_children(&self) -> nr : u16

with
Tracked(owner): Tracked<&NodeOwner<C>>,
requires
self.inner.inner@.invariants(*owner),

Gets the number of valid PTEs in a page table node.

§Verified Properties
§Preconditions
  • The node must be well-formed.
§Postconditions
  • Returns the number of valid PTEs in the node.
§Safety
  • We require the caller to provide a permission token to ensure that this function is only called on a valid page table node.
Source

pub exec fn read_pte(&self, idx: usize) -> pte : C::E

with
Tracked(owner): Tracked<&NodeOwner<C>>,
requires
self.inner.inner@.invariants(*owner),
idx < NR_ENTRIES,
ensures
pte == owner.children_perm.value()[idx as int],

Reads a non-owning PTE at the given index.

A non-owning PTE means that it does not account for a reference count of the a page if the PTE points to a page. The original PTE still owns the child page.

§Safety

The caller must ensure that the index is within the bound.

Source

pub exec fn write_pte(&mut self, idx: usize, pte: C::E)

with
Tracked(owner): Tracked<&mut NodeOwner<C>>,
requires
old(self).inner.inner@.invariants(*old(owner)),
idx < NR_ENTRIES,
ensures
owner.inv(),
owner.meta_perm.addr() == old(owner).meta_perm.addr(),
owner.level == old(owner).level,
owner.meta_own == old(owner).meta_own,
owner.meta_perm.points_to == old(owner).meta_perm.points_to,
owner.children_perm.value() == old(owner).children_perm.value().update(idx as int, pte),
*self == *old(self),

Writes a page table entry at a given index.

This operation will leak the old child if the old PTE is present.

§Safety

The caller must ensure that:

  1. The index must be within the bound;
  2. The PTE must represent a valid Child whose level is compatible with the page table node.
  3. The page table node will have the ownership of the Child after this method.

Methods from Deref<Target = Frame<M>>§

Source

pub exec fn meta(&self) -> &'a M

with
Tracked(perm): Tracked<&'a PointsTo<MetaSlot, Metadata<M>>>,
requires
self.ptr.addr() == perm.addr(),
self.ptr == perm.points_to.pptr(),
perm.is_init(),
perm.wf(&perm.inner_perms),

Gets the metadata of this page.

§Verified Properties
§Preconditions
  • The caller must have a valid permission for the frame.
§Postconditions
  • The function returns the metadata of the frame.
§Safety
  • By requiring the caller to provide a typed permission, we ensure that the metadata is of type M. While a non-verified caller cannot be trusted to obey this interface, all functions that return a Frame<M> also return an appropriate permission.
Source

pub exec fn start_paddr(&self) -> Paddr

with
Tracked(perm): Tracked<&vstd::simple_pptr::PointsTo<MetaSlot>>,
requires
perm.addr() == self.ptr.addr(),
perm.is_init(),
FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end,
perm.addr() % META_SLOT_SIZE == 0,

Gets the physical address of the start of the frame.

Source

pub exec fn map_level(&self) -> PagingLevel

Gets the map level of this page.

This is the level of the page table entry that maps the frame, which determines the size of the frame.

Currently, the level is always 1, which means the frame is a regular page frame.

Source

pub exec fn size(&self) -> usize

Gets the size of this page in bytes.

Source

pub exec fn reference_count(&self) -> u64

with
Tracked(slot_own): Tracked<&mut MetaSlotOwner>,
Tracked(perm): Tracked<&PointsTo<MetaSlot, Metadata<M>>>,
requires
perm.addr() == self.ptr.addr(),
perm.points_to.pptr() == self.ptr,
perm.is_init(),
perm.wf(&perm.inner_perms),
perm.inner_perms.ref_count.id() == perm.points_to.value().ref_count.id(),

Gets the reference count of the frame.

It returns the number of all references to the frame, including all the existing frame handles (Frame, Frame<dyn AnyFrameMeta>), and all the mappings in the page table that points to the frame.

§Verified Properties
§Preconditions
  • Safety Invariant: Metaslot region invariants must hold.
  • Bookkeeping: The caller must have a valid and well-typed permission for the frame.
§Postconditions
  • Correctness: The function returns the reference count of the frame.
§Safety
  • The function is safe to call, but using it requires extra care. The reference count can be changed by other threads at any time including potentially between calling this method and acting on the result.
Source

pub exec fn borrow(&self) -> res : FrameRef<'a, M>

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(perm): Tracked<&MetaPerm<M>>,
requires
old(regions).inv(),
old(regions).slot_owners[self.index()].raw_count == 1,
old(regions).slot_owners[self.index()].self_addr == self.ptr.addr(),
perm.points_to.pptr() == self.ptr,
perm.points_to.value().wf(old(regions).slot_owners[self.index()]),
perm.is_init(),
self.inv(),
ensures
regions.inv(),
res.inner@.ptr.addr() == self.ptr.addr(),
regions.slots =~= old(regions).slots,
regions.slot_owners =~= old(regions).slot_owners,

Borrows a reference from the given frame.

§Verified Properties
§Preconditions
  • Safety Invariant: Metaslot region invariants must hold.
  • Bookkeeping: The caller must have a valid and well-typed permission for the frame.
§Postconditions
  • Safety Invariant: Metaslot region invariants hold after the call.
  • Correctness: The function returns a reference to the frame.
  • Correctness: The system context is unchanged.
Source

pub exec fn slot(&self) -> slot : &'a MetaSlot

with
Tracked(slot_perm): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
requires
slot_perm.pptr() == self.ptr,
slot_perm.is_init(),

Gets the metadata slot of the frame.

§Verified Properties
§Preconditions
  • Safety: The caller must have a valid permission for the frame.
§Postconditions
  • Correctness: The function returns a reference to the metadata slot of the frame.
§Safety
  • There is no way to mutably borrow the metadata slot, so taking an immutable reference is safe. (The fields of the slot can be mutably borrowed, but not the slot itself.)

Trait Implementations§

Source§

impl<'rcu, C: PageTableConfig> Deref for PageTableGuard<'rcu, C>

Source§

exec fn deref(&self) -> &Self::Target

Source§

type Target = FrameRef<'rcu, PageTablePageMeta<C>>

The resulting type after dereferencing.
Source§

impl<'rcu, C: PageTableConfig> TrackDrop for PageTableGuard<'rcu, C>

Source§

open spec fn constructor_requires(self, s: Self::State) -> bool

{ s.lock_held(self.inner.inner@.ptr.addr()) }
Source§

open spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool

{ s1.guards == s0.guards.remove(self.inner.inner@.ptr.addr()) }
Source§

proof fn constructor_spec(self, tracked s: &mut Self::State)

Source§

open spec fn drop_requires(self, s: Self::State) -> bool

{ s.unlocked(self.inner.inner@.ptr.addr()) }
Source§

open spec fn drop_ensures(self, s0: Self::State, s1: Self::State) -> bool

{ s1.guards == s0.guards.insert(self.inner.inner@.ptr.addr(), None) }
Source§

proof fn drop_spec(self, tracked s: &mut Self::State)

Source§

type State = Guards<'rcu, C>

Auto Trait Implementations§

§

impl<'rcu, C> Freeze for PageTableGuard<'rcu, C>

§

impl<'rcu, C> !RefUnwindSafe for PageTableGuard<'rcu, C>

§

impl<'rcu, C> Send for PageTableGuard<'rcu, C>

§

impl<'rcu, C> Sync for PageTableGuard<'rcu, C>

§

impl<'rcu, C> Unpin for PageTableGuard<'rcu, C>
where C: Unpin,

§

impl<'rcu, C> !UnwindSafe for PageTableGuard<'rcu, C>

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
§

impl<T> DerefSpec for T
where T: Deref,

§

fn deref_spec(&self) -> &<T as Deref>::Target

§

fn deref_spec_eq(&self)

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<P, T> Receiver for P
where P: Deref<Target = T> + ?Sized, T: ?Sized,

Source§

type Target = T

🔬This is a nightly-only experimental API. (arbitrary_self_types)
The target type on which the method may be called.
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>