Struct UniqueFrame 

pub struct UniqueFrame<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<M>,
    pub tracked_slot_perm: Tracked<&'static PointsTo<MetaSlot>>,
    pub tracked_metadata_perm: Tracked<Option<MetadataPerm>>,
}

Fields

ptr: PPtr<MetaSlot>

_marker: PhantomData<M>

tracked_slot_perm: Tracked<&'static PointsTo<MetaSlot>>

The permission to access the MetaSlot fields.

tracked_metadata_perm: Tracked<Option<MetadataPerm>>

The complete permission for the currently installed metadata.

Implementations

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

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

with

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

requires

old(regions).contains(frame_to_index(paddr)),

old(regions).slot_owner(paddr).usage is Unused,

old(regions).inv(),

<M as OwnerOf>::wf(metadata, meta_own_in),

ensures

res matches Ok(
    res,
) ==> {
    &&& owner@ is Some
    &&& res.wf(owner@->0)
    &&& res.wf_with_region(owner@->0, *final(regions))
    &&& owner@->0.meta_own == meta_own_in
    &&& res.meta_value(owner@->0) == metadata
    &&& res.inv()
    &&& res.start_paddr_spec() == paddr

},

res is Err
    ==> {
        &&& owner@ is None
        &&& *final(regions) == *old(regions)

    },

final(regions).inv(),

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.

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>
    &&& transmuted.tracked_slot_perm@ == self.tracked_slot_perm@
    &&& transmuted.tracked_metadata_perm@ == self.tracked_metadata_perm@

}

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

ensures

Self::transmute_spec(self, res),

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>,
Tracked(meta_own_in): Tracked<M1::Owner>,
Tracked(repr_perm_in): Tracked<M1::ReprPerm>,
->
new_owner: Tracked<UniqueFrameOwner<M1>>,

requires

self.wf_with_region(owner, *old(regions)),

old(regions).slot_owners[self.index()].in_list_perm.value() == 0,

old(regions).inv(),

self.inv(),

owner.inv(),

<M1 as OwnerOf>::wf(metadata, meta_own_in),

ensures

res.wf(new_owner@),

res.wf_with_region(new_owner@, *final(regions)),

new_owner@.meta_own == meta_own_in,

res.meta_value(new_owner@) == 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.

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

with

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

requires

owner.inv(),

self.inv(),

self.wf(*owner),

self.meta_wf(*owner),

ensures

self.meta_value(*owner) == l,

Gets the metadata of this page.

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.

pub exec fn meta_mut<'a>(&'a mut self) -> res : &'a mut M

with

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

requires

old(self).inv(),

old(self).wf(*owner),

old(self).meta_wf(*owner),

owner.inv(),

ensures

*res == old(self).meta_value(*old(owner)),

*final(res) == final(self).meta_value(*final(owner)),

final(self).inv(),

final(self).ptr == old(self).ptr,

final(self).tracked_slot_perm@ == old(self).tracked_slot_perm@,

final(owner).meta_own == old(owner).meta_own,

final(owner).slot_index == old(owner).slot_index,

final(owner).inv(),

final(self).meta_wf(*final(owner)),

(*final(self)).wf(*final(owner)),

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])

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

pub const exec fn size(&self) -> usize

returns

PAGE_SIZE,

Gets the size of this page in bytes.

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

returns

1u8,

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.

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

pub exec fn start_paddr(&self) -> Paddr

requires

self.ptr_inv(),

returns

meta_to_frame(self.ptr.addr()),

Gets the physical address of the start of the frame.

pub exec fn reset_as_unused(self)

with

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

requires

self.inv(),

owner.inv(),

regions.inv(),

self.wf_with_region(owner, *old(regions)),

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

ensures

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.

pub exec fn slot<'a>(&self) -> &'a MetaSlot

requires

self.ptr_inv(),

returns

self.tracked_slot_perm@.value(),

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

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

frame.wf_with_region(*old(regions)),

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>.

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> UniqueFrame<Link<M>>

pub open spec fn frame_link_inv( self, owner: UniqueFrameOwner<Link<M>>, regions: MetaRegionOwners, ) -> bool

{
    &&& self.meta_value(owner).prev is None
    &&& self.meta_value(owner).next is None
    &&& owner.meta_own.paddr == regions.slots[owner.slot_index].addr()
    &&& regions.slot_owners[owner.slot_index].in_list_perm.value() == 0

}

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

pub open spec fn start_paddr_spec(self) -> Paddr

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

pub open spec fn index(self) -> int

{ frame_to_index(self.start_paddr_spec()) }

pub open spec fn metadata_perm(self) -> MetadataPerm

{ self.tracked_metadata_perm@->0 }

The complete metadata permission carried by this unique handle.

pub open spec fn slot_perm(self) -> PointsTo<MetaSlot>

{ *self.tracked_slot_perm@ }

The metadata-slot permission carried by this unique handle.

pub open spec fn ptr_inv(self) -> bool

{
    &&& valid_frame_paddr(self.start_paddr_spec())
    &&& 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.slot_perm().pptr() == self.ptr
    &&& self.slot_perm().is_init()

}

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

pub open spec fn meta_wf(self, owner: UniqueFrameOwner<M>) -> bool

{ typed_meta_wf::<M>(self.slot_perm(), self.metadata_perm(), owner.repr_perm->0) }

pub open spec fn meta_value(self, owner: UniqueFrameOwner<M>) -> M

{ typed_meta_value::<M>(self.metadata_perm(), owner.repr_perm->0) }

pub open spec fn wf_with_region( self, owner: UniqueFrameOwner<M>, s: MetaRegionOwners, ) -> bool

{
    let idx = owner.slot_index;
    let so = s.slot_owners[idx];
    &&& self.wf(owner)
    &&& s.contains(idx)
    &&& self.tracked_slot_perm@ == s.slots[idx]
    &&& self.meta_wf(owner)
    &&& self.meta_value(owner).wf(owner.meta_own)
    &&& so.metadata_perm.is_resource_vacant()
    &&& so.ref_count() == REF_COUNT_UNIQUE
    &&& so.usage is Frame
    &&& so.paths_in_pt.is_empty()

}

Cross-object validity of a live UNIQUE handle against the region map — the UniqueFrame analog of Frame::wf_with_region (which covers the SHARED state).

Trait Implementations

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

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

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

open spec fn inv(self) -> bool

{
    &&& self.ptr_inv()
    &&& self.tracked_metadata_perm@ is Some
    &&& MetaSlot::perms_related(self.slot_perm(), self.metadata_perm())

}

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

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

{
    &&& self.ptr.addr() == index_to_meta(owner.slot_index)

}

type Owner = UniqueFrameOwner<M>

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

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

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

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

exec fn try_from(frame: Frame<M>) -> Result<Self, Self::Error>

Tries to get a unique frame from a shared frame.

If the reference count is not 1, the frame is returned back.

type Error = Frame<M>

The type returned in the event of a conversion error.