Struct Frame Ref &nbsp; Copy item path

impl<M: AnyFrameMeta> FrameRef<'_, M>

pub exec fn borrow_paddr(raw: Paddr) -> r : Self

with

Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(perm): Tracked <& MetaPerm <M>>,

requires

raw % PAGE_SIZE() == 0,

raw < MAX_PADDR(),

!old(regions).slots.contains_key(frame_to_index(raw)),

old(regions).inv(),

ensures

regions.inv(),

manually_drop_deref_spec(&r.inner.0).ptr.addr() == frame_to_meta(raw),

Borrows the Frame at the physical address as a FrameRef.

§Safety

The caller must ensure that:

the frame outlives the created reference, so that the reference can be seen as borrowed from that frame.
the type of the FrameRef (M) matches the borrowed frame.

impl<'a, C: PageTableConfig> FrameRef<'a, PageTablePageMeta<C>>

pub exec fn lock<'rcu, A: InAtomicMode>( self, _guard: &'rcu A, ) -> PPtr<PageTableGuard<'rcu, C>>
where 'a: 'rcu,

with

Tracked(guards): Tracked <& mut Guards <'rcu,C>>,
->
guard_perm: Tracked <GuardPerm <'rcu,C>>,

Locks the page table node.

An atomic mode guard is required to

prevent deadlocks;
provide a lifetime ('rcu) that the nodes are guaranteed to outlive.

pub exec fn make_guard_unchecked<'rcu, A: InAtomicMode>( self, _guard: &'rcu A, ) -> res : PPtr<PageTableGuard<'rcu, C>>
where 'a: 'rcu,

with

Tracked(owner): Tracked <& NodeOwner <C>>,
Tracked(guards): Tracked <& mut Guards <'rcu,C>>,
->
guard_perm: Tracked <GuardPerm <'rcu,C>>,

requires

owner.inv(),

self.inner@.wf(*owner),

!old(guards).guards.contains_key(owner.meta_perm.addr()),

old(guards).unlocked(owner.meta_perm.addr()),

ensures

guards.lock_held(owner.meta_perm.addr()),

OwnerSubtree::implies(
    CursorOwner::node_unlocked(*old(guards)),
    CursorOwner::node_unlocked_except(*guards, owner.meta_perm.addr()),
),

forall |i: usize| old(guards).lock_held(i) ==> guards.lock_held(i),

res.addr() == guard_perm@.addr(),

owner.relate_guard_perm(guard_perm@),

Creates a new PageTableGuard without checking if the page table lock is held.

§Safety

This function must be called if this task logically holds the lock.

Calling this function when a guard is already created is undefined behavior unless that guard was already forgotten.

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

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

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.

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.

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.

pub exec fn size(&self) -> usize

Gets the size of this page in bytes.

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.

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.

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§

impl<M: AnyFrameMeta> Deref for FrameRef<'_, M>

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

type Target = Frame<M>

The resulting type after dereferencing.

Auto Trait Implementations§

impl<'a, M> !UnwindSafe for FrameRef<'a, M>

Blanket Implementations§

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

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

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

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

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

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)

impl<T> From<T> for T

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

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

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 for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<P, T> Receiver for P
where P: Deref<Target = T> + ?Sized, T: ?Sized,

type Target = T

🔬This is a nightly-only experimental API. (arbitrary_self_types)

The target type on which the method may be called.

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

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom>::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>

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

type Error = >::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, >::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 for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool