Skip to main content

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<'a>(&'a mut self, idx: usize) -> res : Entry<'a, 'rcu, C>

with
Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(child_owner): Tracked<&EntryOwner<C>>,
Tracked(regions): Tracked<&MetaRegionOwners>,
requires
owner.inv(),
!child_owner.in_scope,
child_owner.inv(),
owner.relate_guard(*old(self)),
child_owner.match_pte(owner.children_perm.value()[idx as int], child_owner.parent_level),
regions.inv(),
regions.slots.contains_key(owner.slot_index),
idx < NR_ENTRIES,
ensures
res.wf(*child_owner),
res.idx == idx,
owner.relate_guard(*res.node),
*final(self) == *old(self),

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>>,
Tracked(regions): Tracked<&MetaRegionOwners>,
requires
self.inner.inner@.invariants(*owner),
regions.inv(),
owner.metaregion_sound_node(*regions),
returns
owner.meta_own.nr_children.value(),

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 unsafe exec fn read_pte(&self, idx: usize) -> pte : C::E

with
Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(regions): Tracked<&MetaRegionOwners>,
requires
self.inner.inner@.invariants(*owner),
regions.inv(),
regions.slots.contains_key(owner.slot_index),
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 unsafe exec fn write_pte(&mut self, idx: usize, pte: C::E)

with
Tracked(owner): Tracked<&mut NodeOwner<C>>,
Tracked(regions): Tracked<&MetaRegionOwners>,
requires
old(self).inner.inner@.invariants(*old(owner)),
regions.inv(),
regions.slots.contains_key(old(owner).slot_index),
idx < NR_ENTRIES,
ensures
final(owner).inv(),
final(owner).level == old(owner).level,
final(owner).meta_own == old(owner).meta_own,
final(owner).slot_index == old(owner).slot_index,
final(owner).children_perm.value()
    == old(owner).children_perm.value().update(idx as int, pte),
*final(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),
returns
perm.value().metadata,

Gets the metadata of this page.

§Verified Properties
§Preconditions
  • The caller must have a valid permission for the frame.
§Postconditions
  • The function returns the borrowed 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,
returns
meta_to_frame(self.ptr.addr()),

Gets the physical address of the start of the frame.

§Verified Properties
§Preconditions
  • Bookkeeping: takes the permission for the frame’s metadata slot.
§Postconditions
  • Correctness: returns the physical address of the frame.
§Safety

The caller cannot obtain a frame that doesn’t have a valid permission, and this function does not mutate any state, so it is always sound to call.

Source

pub exec fn eq(&self, other: &Self) -> res : bool

with
Tracked(regions): Tracked<&MetaRegionOwners>,
requires
self.inv(),
other.inv(),
regions.inv(),
ensures
res == (meta_to_frame(self.ptr.addr()) == meta_to_frame(other.ptr.addr())),

Compares two frames by their start physical address.

§Verified Properties
§Preconditions
  • Safety Invariant: the frames and metadata regions must satisfy the global invariants.
§Postconditions
  • Correctness: the function returns true if the frames have the same physical addresses and false otherwise.
§Safety

Everything is immutable, so the safety invariant is preserved implicitly.

§Verification Design

This is an inherent impl equivalent to PartialEq::eq for Frame<M>: freed from the trait signature so that this version can thread the tracked MetaRegionOwners via verus_spec.

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(),
returns
perm.value().ref_count,

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>,
requires
self.inv_with_regions(*old(regions)),
ensures
final(regions).inv(),
res.inner@.ptr.addr() == self.ptr.addr(),
final(regions).slot_owners =~= old(regions).slot_owners,
final(regions).slots =~= old(regions).slots,
final(regions).frame_obligations =~= old(regions).frame_obligations,

Borrows a reference from the given frame.

§Verified Properties
§Preconditions
  • Safety Invariant: Metaslot region invariants must hold.
§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(),
returns
slot_perm.value(),

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

returns
self.inner,
Source§

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

The resulting type after dereferencing.
Source§

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

Source§

type Key = usize

The node address whose lock this guard holds. The token thus identifies which guard it tracks; drop_requires’s key match prevents a guard’s obligation from being used to drop a different guard. The real lock-set ledger is Guards::guards; this trait’s discipline lifts the existing state-side discipline onto the obligation token by carrying the locked address.

Source§

open spec fn key(self) -> Self::Key

{ self.inner.inner@.ptr.addr() }
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, obl_key: Self::Key, ) -> bool

{
    &&& s1.guards == s0.guards.remove(self.inner.inner@.ptr.addr())
    &&& obl_key == self.inner.inner@.ptr.addr()

}
Source§

proof fn constructor_spec(self, tracked s: &mut Self::State) -> tracked obl : DropObligation<Self::Key>

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, obl_key: Self::Key, ) -> bool

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

open spec fn consume_requires(self, s: Self::State, obl_key: Self::Key) -> bool

{ obl_key == self.inner.inner@.ptr.addr() }
Source§

open spec fn consume_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

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

proof fn consume_obligation(self, tracked s: &mut Self::State, tracked obl: DropObligation<Self::Key>)

Source§

type State = Guards<'rcu>

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> UnsafeUnpin for PageTableGuard<'rcu, C>

§

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

Blanket Implementations§

§

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

§

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

👎Deprecated: If you can, do not use this module as it adds assumptions about the core of Rust’s deref semantics.
§

fn deref_spec_eq(&self)

👎Deprecated: If you can, do not use this module as it adds assumptions about the core of Rust’s deref semantics.
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<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>

§

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