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.inv(),
owner.relate_guard_perm(*guard_perm),
guard_perm.addr() == guard.addr(),
idx < NR_ENTRIES(),
child_owner.match_pte(owner.children_perm.value()[idx as int], child_owner.parent_level),
ensures
res.wf(*child_owner),
res.node.addr() == guard_perm.addr(),

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 <& mut NodeOwner <C>>,
requires
self.inner.inner@.ptr.addr() == old(owner).meta_perm.addr(),
self.inner.inner@.ptr.addr() == old(owner).meta_perm.points_to.addr(),
old(owner).inv(),
ensures
*owner == *old(owner),

Gets the number of valid PTEs in the node.

Source

pub exec fn stray_mut(&mut self) -> PCell<bool>

with
Tracked(owner): Tracked <EntryOwner <C>>,
requires
owner.is_node(),
old(self).inner.inner@.ptr.addr() == owner.node.unwrap().meta_perm.addr(),
old(self).inner.inner@.ptr.addr() == owner.node.unwrap().meta_perm.points_to.addr(),
owner.inv(),

Returns if the page table node is detached from its parent.

Source

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

with
Tracked(owner): Tracked <& NodeOwner <C>>,
requires
self.inner.inner@.ptr.addr() == owner.meta_perm.addr(),
self.inner.inner@.ptr.addr() == owner.meta_perm.points_to.addr(),
owner.inv(),
meta_to_frame(owner.meta_perm.addr) < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
FRAME_METADATA_RANGE().start <= owner.meta_perm.addr < FRAME_METADATA_RANGE().end,
owner.meta_perm.addr % META_SLOT_SIZE() == 0,
idx < NR_ENTRIES(),
owner.children_perm.addr() == paddr_to_vaddr(meta_to_frame(owner.meta_perm.addr)),
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(owner).inv(),
meta_to_frame(old(owner).meta_perm.addr)
    < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
idx < NR_ENTRIES(),
ensures
owner.inv(),
owner.meta_perm.addr() == old(owner).meta_perm.addr(),
owner.meta_own == old(owner).meta_own,
owner.meta_perm.points_to == old(owner).meta_perm.points_to,
*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_pt<'a, C: PageTableConfig>( &'a self, verus_tmp_p_slot: Tracked<&'a PointsTo<MetaSlot>>, owner: MetaSlotOwner, ) -> res : &'a PageTablePageMeta<C>

requires
self.inv(),
p_slot.pptr() == self.ptr,
p_slot.is_init(),
p_slot.value().wf(owner),
is_variant(owner.view().storage.value(), "PTNode"),
Source

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

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

Gets the metadata of this page.

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(slot_perm): Tracked <& vstd ::simple_pptr ::PointsTo <MetaSlot>>,
requires
slot_perm.pptr() == self.ptr,
slot_perm.is_init(),
old(slot_own).ref_count.is_for(slot_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.

§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(),
self.paddr() % PAGE_SIZE() == 0,
self.paddr() < MAX_PADDR(),
!old(regions).slots.contains_key(self.index()),
perm.points_to.pptr() == self.ptr,
perm.is_init(),
FRAME_METADATA_RANGE().start <= perm.points_to.addr() < FRAME_METADATA_RANGE().end,
perm.points_to.addr() % META_SLOT_SIZE() == 0,
ensures
regions.inv(),
res.inner@.ptr.addr() == self.ptr.addr(),

Borrows a reference from the given frame.

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(),

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> Undroppable 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§

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>