Frame

ostd::mm::frame

Struct Frame 

Source 
#[repr(transparent)]
pub struct Frame<M: AnyFrameMeta> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<M>,
}
Expand description

A smart pointer to a frame.

A frame is a contiguous range of bytes in physical memory. The Frame type is a smart pointer to a frame that is reference-counted.

Frames are associated with metadata. The type of the metadata M is determines the kind of the frame. If M implements [AnyUFrameMeta], the frame is a untyped frame. Otherwise, it is a typed frame.

Fields§

§ptr: PPtr<MetaSlot>§_marker: PhantomData<M>

Implementations§

Source§

impl<M: AnyFrameMeta> Frame<M>

Source

pub open spec fn paddr(self) -> usize

{ meta_to_frame(self.ptr.addr()) }
Source

pub open spec fn index(self) -> usize

{ frame_to_index(self.paddr()) }
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§

impl<'a, M: AnyFrameMeta> Frame<M>

Source

pub open spec fn from_unused_requires( regions: MetaRegionOwners, paddr: Paddr, metadata: M, ) -> bool

{
    &&& paddr % PAGE_SIZE() == 0
    &&& paddr < MAX_PADDR()
    &&& regions.slots.contains_key(frame_to_index(paddr))
    &&& regions.slot_owners[frame_to_index(paddr)].usage is Unused
    &&& regions.slot_owners[frame_to_index(paddr)].in_list.points_to(0)
    &&& regions.slot_owners[frame_to_index(paddr)].self_addr == frame_to_meta(paddr)
    &&& regions.inv()

}
Source

pub open spec fn from_unused_ensures( old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, paddr: Paddr, metadata: M, r: Self, ) -> bool

{
    &&& new_regions@
        == MetaSlot::get_from_unused_spec::<M>(paddr, metadata, false, old_regions@).1
    &&& new_regions.inv()
    &&& forall |paddr: Paddr| {
        #[trigger] old_regions.slots.contains_key(frame_to_index(paddr))
            ==> new_regions.slots.contains_key(frame_to_index(paddr))
    }

}
Source

pub exec fn from_unused(paddr: Paddr, metadata: M) -> r : Result<Self, GetFrameError>

with
Tracked(regions): Tracked <& mut MetaRegionOwners>,
requires
Self::from_unused_requires(*old(regions), paddr, metadata),
ensures
r matches Ok(
    r,
) ==> Self::from_unused_ensures(*old(regions), *regions, paddr, metadata, r),

Gets a Frame with a specific usage from a raw, unused page.

The caller should provide the initial metadata of the page.

If the provided frame is not truly unused at the moment, it will return an error. If wanting to acquire a frame that is already in use, use Frame::from_in_use instead.

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§

impl<M: AnyFrameMeta> Frame<M>

Source

pub exec fn from_in_use(paddr: Paddr) -> Result<Self, GetFrameError>

with
Tracked(regions): Tracked <& mut MetaRegionOwners>,

Gets a dynamically typed Frame from a raw, in-use page.

If the provided frame is not in use at the moment, it will return an error.

The returned frame will have an extra reference count to the frame.

Source

pub open spec fn from_raw_requires(regions: MetaRegionOwners, paddr: Paddr) -> bool

{
    &&& paddr % PAGE_SIZE() == 0
    &&& !regions.slots.contains_key(frame_to_index(paddr))
    &&& regions.dropped_slots.contains_key(frame_to_index(paddr))
    &&& regions.inv()

}
Source

pub open spec fn from_raw_ensures( old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, paddr: Paddr, r: Self, ) -> bool

{
    &&& new_regions.inv()
    &&& new_regions.slots.contains_key(frame_to_index(paddr))
    &&& !new_regions.dropped_slots.contains_key(frame_to_index(paddr))
    &&& new_regions.slots[frame_to_index(paddr)]
        == old_regions.dropped_slots[frame_to_index(paddr)]
    &&& forall |i: usize| {
        i != frame_to_index(paddr) ==> new_regions.slots[i] == old_regions.slots[i]
    }
    &&& forall |i: usize| {
        i != frame_to_index(paddr)
            ==> new_regions.dropped_slots[i] == old_regions.dropped_slots[i]
    }
    &&& new_regions.slot_owners == old_regions.slot_owners
    &&& r.ptr == new_regions.slots[frame_to_index(paddr)].pptr()
    &&& r.paddr() == paddr

}
Source

pub open spec fn into_raw_requires(self, regions: MetaRegionOwners) -> bool

{
    &&& regions.slots.contains_key(self.index())
    &&& !regions.dropped_slots.contains_key(self.index())
    &&& regions.inv()

}
Source

pub open spec fn into_raw_ensures( self, regions: MetaRegionOwners, r: Paddr, perm: MetaPerm<M>, ) -> bool

{
    &&& r == meta_to_frame(self.ptr.addr())
    &&& regions.slot_owners == regions.slot_owners
    &&& regions.dropped_slots == regions.dropped_slots
    &&& forall |i: usize| {
        i != frame_to_index(self.ptr.addr()) ==> regions.slots[i] == regions.slots[i]
    }

}
Source§

impl<'a, M: AnyFrameMeta> Frame<M>

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 const 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 const 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 into_raw(self) -> r : Paddr

with
Tracked(regions): Tracked <& mut MetaRegionOwners>,
->
frame_perm: Tracked <MetaPerm <M>>,
requires
Self::into_raw_requires(self, *old(regions)),
ensures
Self::into_raw_ensures(self, *regions, r, frame_perm@),

Forgets the handle to the frame.

This will result in the frame being leaked without calling the custom dropper.

A physical address to the frame is returned in case the frame needs to be restored using Frame::from_raw later. This is useful when some architectural data structures need to hold the frame handle such as the page table.

Source

pub exec fn from_raw(paddr: Paddr) -> r : Self

with
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(perm): Tracked <& MetaPerm <M>>,
requires
Self::from_raw_requires(*old(regions), paddr),
ensures
Self::from_raw_ensures(*old(regions), *regions, paddr, r),

Restores a forgotten Frame from a physical address.

§Safety

The caller should only restore a Frame that was previously forgotten using Frame::into_raw.

And the restoring operation should only be done once for a forgotten Frame. Otherwise double-free will happen.

Also, the caller ensures that the usage of the frame is correct. There’s no checking of the usage in this function.

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

impl<C: PageTableConfig> Frame<PageTablePageMeta<C>>

Source

pub exec fn level(&self) -> PagingLevel

with
Tracked(perm): Tracked <& PointsTo <MetaSlot,PageTablePageMeta <C>>>,
requires
self.ptr.addr() == perm.addr(),
self.ptr.addr() == perm.points_to.addr(),
perm.is_init(),
perm.wf(),
Source

pub exec fn alloc(level: PagingLevel) -> res : Self

with
Tracked(regions): Tracked <& mut MetaRegionOwners>,
->
owner: Tracked <OwnerSubtree <C>>,
requires
level <= NR_LEVELS(),
old(regions).inv(),
ensures
regions.inv(),

Allocates a new empty page table node.

Source§

impl<M: AnyFrameMeta + Repr<MetaSlot> + OwnerOf> Frame<M>

Source

pub open spec fn from_raw_spec(paddr: Paddr) -> Self

{
    Frame::<M> {
        ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
        _marker: PhantomData,
    }
}

Trait Implementations§

Source§

impl<M: AnyFrameMeta> Clone for Frame<M>

Source§

exec fn clone(&self) -> Self

1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
Source§

impl<M: AnyFrameMeta> Inv for Frame<M>

Source§

open spec fn inv(self) -> bool

{
    &&& self.ptr.addr() % META_SLOT_SIZE() == 0
    &&& FRAME_METADATA_RANGE().start <= self.ptr.addr()
        < FRAME_METADATA_RANGE().start + MAX_NR_PAGES() * META_SLOT_SIZE()
    &&& self.ptr.addr() < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR()

}
Source§

impl<M: AnyFrameMeta> Repr<MetaSlot> for Frame<M>

Source§

open spec fn wf(m: MetaSlot) -> bool

{ true }
Source§

open spec fn to_repr_spec(self) -> MetaSlot

{ arbitrary() }
Source§

open spec fn from_repr_spec(r: MetaSlot) -> Self

{ arbitrary() }
Source§

exec fn to_repr(self) -> res : MetaSlot

ensures
res == self.to_repr_spec(),
Source§

exec fn from_repr(r: MetaSlot) -> res : Self

ensures
res == Self::from_repr_spec(r),
Source§

exec fn from_borrowed<'a>(r: &'a MetaSlot) -> res : &'a Self

ensures
*res == Self::from_repr_spec(*r),
Source§

proof fn from_to_repr(self)

ensures
Self::from_repr(self.to_repr()) == self,
Source§

proof fn to_from_repr(r: MetaSlot)

ensures
Self::from_repr(r).to_repr() == r,
Source§

proof fn to_repr_wf(self)

ensures
Self::wf(self.to_repr()),
Source§

impl<M: AnyFrameMeta> Undroppable for Frame<M>

Source§

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

{
    &&& s.slots.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& !s.dropped_slots.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s.inv()

}
Source§

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

{
    &&& !s1.slots.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s1.dropped_slots.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s0.slot_owners == s1.slot_owners
    &&& forall |i: usize| {
        i != frame_to_index(meta_to_frame(self.ptr.addr()))
            ==> s0.dropped_slots[i] == s1.dropped_slots[i] && s0.slots[i] == s1.slots[i]
    }
    &&& s1.dropped_slots[frame_to_index(meta_to_frame(self.ptr.addr()))]
        == s0.slots[frame_to_index(meta_to_frame(self.ptr.addr()))]
    &&& s1.inv()

}
Source§

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

Source§

type State = MetaRegionOwners

Auto Trait Implementations§

§

impl<M> Freeze for Frame<M>

§

impl<M> !RefUnwindSafe for Frame<M>

§

impl<M> Send for Frame<M>
where M: Send,

§

impl<M> Sync for Frame<M>
where M: Sync,

§

impl<M> Unpin for Frame<M>
where M: Unpin,

§

impl<M> UnwindSafe for Frame<M>
where M: 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> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. 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> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
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>