ostd::mm::frame::unique

Struct UniqueFrame

pub struct UniqueFrame<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<M>,
}

Fields§

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

Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M>

Source

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

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
->
owner: Tracked<Option<UniqueFrameOwner<M>>>,

requires

old(regions).slots.contains_key(frame_to_index(paddr)),

old(regions).slot_owners.contains_key(frame_to_index(paddr)),

old(regions).slot_owners[frame_to_index(paddr)].usage is Unused,

old(regions).inv(),

ensures

!has_safe_slot(paddr) ==> res is Err,

res is Ok ==> res.unwrap().wf(owner@.unwrap()),

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

The caller should provide the initial metadata of the page.

§Verified Properties

§Preconditions

The page must be unused and the metadata region must be well-formed.

§Postconditions

If the page is valid, the function returns a unique frame.

§Safety

If paddr is misaligned or out of bounds, the function will return an error. If it returns a frame, it also returns an owner for that frame, indicating that the caller now has exclusive ownership of it. See [Safe Encapsulation] for more details.

Source

pub open spec fn transmute_spec<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>( self, transmuted: UniqueFrame<M1>, ) -> bool

{
    &&& transmuted.ptr.addr() == self.ptr.addr()
    &&& transmuted._marker == PhantomData::<M1>

}

Source

pub exec fn transmute<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>( self, ) -> res : UniqueFrame<M1>

ensures

Self::transmute_spec(self, res),

Source

pub exec fn repurpose<M1: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf>( self, metadata: M1, ) -> res : UniqueFrame<M1>

with

Tracked(owner): Tracked<UniqueFrameOwner<M>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
->
new_owner: Tracked<UniqueFrameOwner<M1>>,

requires

self.wf(owner),

owner.inv(),

owner.global_inv(*old(regions)),

old(regions).slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr()))),

old(regions)
    .slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))]
    .inner_perms
    .ref_count
    .value() == REF_COUNT_UNIQUE,

old(regions).inv(),

ensures

res.wf(new_owner@),

new_owner@.meta_perm.value().metadata == metadata,

final(regions).inv(),

Repurposes the frame with a new metadata.

§Verified Properties

§Preconditions

The caller must provide a valid owner for the frame, and the metadata region invariants must hold.
The meta slot’s reference count must be REF_COUNT_UNIQUE.

§Postconditions

The function returns a new owner for the frame with the new metadata, and the metadata region invariants are preserved.

§Safety

The existence of a valid owner guarantees that the memory is initialized with metadata of type M, and represents that the caller has exclusive ownership of the frame.

Source

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

with

Tracked(owner): Tracked<&'a UniqueFrameOwner<M>>,

requires

owner.inv(),

self.wf(*owner),

ensures

owner.meta_perm.mem_contents().value().metadata == l,

Gets the metadata of this page. Note that this function body differs from the original, because as_meta_ptr returns a ReprPtr<MetaSlot, Metadata<M>> instead of a *M. So in order to keep the immutable borrow, we borrow the metadata value from that pointer.

§Verified Properties

§Preconditions

The caller must provide a valid owner for the frame.

§Postconditions

The function returns the metadata of the frame.

§Safety

The existence of a valid owner guarantees that the memory is initialized with metadata of type M, and represents that the caller has exclusive ownership of the frame.

Source

pub exec fn meta_mut(&mut self) -> res : ReprPtr<MetaSlot, Metadata<M>>

with

Tracked(owner): Tracked<&UniqueFrameOwner<M>>,

requires

owner.inv(),

old(self).wf(*owner),

ensures

res.addr() == final(self).ptr.addr(),

res.ptr.addr() == final(self).ptr.addr(),

*final(self) == *old(self),

Gets the mutable metadata of this page. Verified Properties

§Preconditions

The caller must provide a valid owner for the frame.

§Postconditions

The function returns the mutable metadata of the frame.

§Safety

The existence of a valid owner guarantees that the memory is initialized with metadata of type M, and represents that the caller has exclusive ownership of the frame. (See [Safe Encapsulation])

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf + ?Sized> UniqueFrame<M>

Source

pub exec fn start_paddr(&self) -> Paddr

with

Tracked(owner): Tracked<&UniqueFrameOwner<M>>,

requires

owner.inv(),

self.wf(*owner),

returns

meta_to_frame(self.ptr.addr()),

Gets the physical address of the start of the frame.

Source

pub const exec fn level(&self) -> PagingLevel

Gets the paging 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 open spec fn into_raw_requires(self, regions: MetaRegionOwners) -> bool

{
    &&& regions.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& regions.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count
        == 0
    &&& regions.inv()

}

Source

pub open spec fn into_raw_ensures( self, old_regions: MetaRegionOwners, regions: MetaRegionOwners, r: Paddr, ) -> bool

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

}

Source

pub exec fn reset_as_unused(self)

with

Tracked(owner): Tracked<UniqueFrameOwner<M>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,

requires

self.wf(owner),

owner.inv(),

old(regions).inv(),

old(regions).slot_owners.contains_key(owner.slot_index),

old(regions).slot_owners[owner.slot_index].raw_count == 0,

old(regions).slot_owners[owner.slot_index].self_addr == meta_addr(owner.slot_index),

!old(regions).slots.contains_key(owner.slot_index),

owner.meta_perm.inner_perms.ref_count.value() == REF_COUNT_UNIQUE,

owner.meta_perm.inner_perms.in_list.value() == 0,

owner.meta_perm.inner_perms.storage.is_init(),

owner.meta_perm.inner_perms.vtable_ptr.is_init(),

ensures

final(regions).slot_owners[owner.slot_index].raw_count == 0,

final(regions).inv(),

Resets the frame to unused without up-calling the allocator.

This is solely useful for the allocator implementation/testing and is highly experimental. Usage of this function is discouraged.

Usage of this function other than the allocator would actually leak the frame since the allocator would not be aware of the frame.

Source

pub exec fn slot<'a>(&self) -> &'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(),

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M>

Source

pub exec fn try_from_shared(frame: Frame<M>) -> res : Result<Self, Frame<M>>

with

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

requires

frame.inv(),

old(regions).inv(),

old(regions).slots.contains_key(frame_to_index(meta_to_frame(frame.ptr.addr()))),

old(regions).slot_owners.contains_key(frame_to_index(meta_to_frame(frame.ptr.addr()))),

old(regions).slots[frame_to_index(meta_to_frame(frame.ptr.addr()))].pptr() == frame.ptr,

old(regions)
    .slot_owners[frame_to_index(meta_to_frame(frame.ptr.addr()))]
    .inner_perms
    .ref_count
    .id()
    == old(regions)
        .slots[frame_to_index(meta_to_frame(frame.ptr.addr()))]
        .value()
        .ref_count
        .id(),

ensures

final(regions).slots == old(regions).slots,

final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),

Tries to convert a shared frame into a unique one by CAS’ing ref_count from 1 to REF_COUNT_UNIQUE. Inherent sibling of TryFrom<Frame<M>> for UniqueFrame<M>.

Trait Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> From<UniqueFrame<M>> for Frame<M>

Source §

exec fn from(unique: UniqueFrame<M>) -> Self

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> ModelOf for UniqueFrame<M>

§

fn model(self, owner: Self::Owner) -> <Self::Owner as View>::V

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> OwnerOf for UniqueFrame<M>

Source §

open spec fn wf(self, owner: Self::Owner) -> bool

{
    &&& self.ptr.addr() == owner.meta_perm.addr()

}

Source §

type Owner = UniqueFrameOwner<M>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> TrackDrop for UniqueFrame<M>

Source §

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

{
    &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 0
    &&& s
        .slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))]
        .inner_perms
        .ref_count
        .value() != REF_COUNT_UNUSED
    &&& s.inv()

}

Source §

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

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

}

Source §

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

Source §

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

{
    &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count > 0
    &&& s.inv()

}

Source §

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

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

}

Source §