MetaSlot

ostd::mm::frame::meta

Struct MetaSlot 

Source 
#[repr(C)]
pub struct MetaSlot {
    pub storage: PCell<MetaSlotStorage>,
    pub ref_count: PAtomicU64,
    pub vtable_ptr: PPtr<usize>,
    pub in_list: PAtomicU64,
}

Fields§

§storage: PCell<MetaSlotStorage>

The metadata of a frame.

It is placed at the beginning of a slot because:

  • the implementation can simply cast a *const MetaSlot to a *const AnyFrameMeta for manipulation;
  • if the metadata need special alignment, we can provide at most PAGE_METADATA_ALIGN bytes of alignment;
  • the subsequent fields can utilize the padding of the reference count to save space.

§Verification Design

We model the metadata of the slot as a MetaSlotStorage, which is a tagged union of the different types of metadata defined in the development.

§ref_count: PAtomicU64

The reference count of the page.

Specifically, the reference count has the following meaning:

  • REF_COUNT_UNUSED: The page is not in use.
  • REF_COUNT_UNIQUE: The page is owned by a [UniqueFrame].
  • 0: The page is being constructed ([Frame::from_unused]) or destructured ([drop_last_in_place]).
  • 1..REF_COUNT_MAX: The page is in use.
  • REF_COUNT_MAX..REF_COUNT_UNIQUE: Illegal values to prevent the reference count from overflowing. Otherwise, overflowing the reference count will cause soundness issue.
§vtable_ptr: PPtr<usize>

The virtual table that indicates the type of the metadata. Currently we do not verify this because of the dependency on the dyn Trait pattern. But we can revisit it now that dyn Trait is supported by Verus.

§in_list: PAtomicU64

This is only accessed by crate::mm::frame::linked_list. It stores 0 if the frame is not in any list, otherwise it stores the ID of the list.

It is ugly but allows us to tell if a frame is in a specific list by one relaxed read. Otherwise, if we store it conditionally in storage we would have to ensure that the type is correct before the read, which costs a synchronization.

Implementations§

Source§

impl MetaSlot

Source

pub exec fn cast_slot<M: AnyFrameMeta + Repr<MetaSlotStorage>>( &self, addr: usize, verus_tmp_perm: Tracked<&PointsTo<MetaSlot>>, ) -> res : ReprPtr<MetaSlot, Metadata<M>>

requires
perm.value() == self,
addr == perm.addr(),
ensures
res.ptr.addr() == addr,
res.addr == addr,

A helper function that casts a MetaSlot pointer to a Metadata pointer of type M.

Source

pub exec fn cast_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>( addr: usize, verus_tmp_perm: Tracked<PointsTo<MetaSlot>>, verus_tmp_inner_perms: Tracked<MetadataInnerPerms>, ) -> res : Tracked<PointsTo<MetaSlot, Metadata<M>>>

ensures
res@.addr == addr,
res@.points_to == perm,
res@.inner_perms == inner_perms,

A helper function that casts MetaSlot permission to a Metadata permission of type M.

Source§

impl MetaSlot

Source

pub open spec fn get_from_unused_inner_perms_spec( as_unique: bool, perms: MetadataInnerPerms, ) -> bool

{
    &&& perms.ref_count.value()
        == (if as_unique { REF_COUNT_UNIQUE as u64 } else { 1u64 })
    &&& perms.in_list.value() == 0
    &&& perms.storage.is_init()
    &&& perms.vtable_ptr.is_init()

}
Source

pub open spec fn get_from_unused_spec( paddr: Paddr, as_unique: bool, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool

recommends
paddr % PAGE_SIZE == 0,
paddr < MAX_PADDR,
pre.inv(),
{
    let idx = frame_to_index(paddr);
    {
        &&& post.slots =~= pre.slots.remove(idx)
        &&& MetaSlot::get_from_unused_inner_perms_spec(
            as_unique,
            post.slot_owners[idx].inner_perms,
        )
        &&& post.slot_owners[idx].usage == PageUsage::Frame
        &&& post.slot_owners[idx].raw_count == pre.slot_owners[idx].raw_count
        &&& post.slot_owners[idx].self_addr == pre.slot_owners[idx].self_addr
        &&& post.slot_owners[idx].path_if_in_pt == pre.slot_owners[idx].path_if_in_pt
        &&& forall |i: usize| {
            i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
        }

    }
}
Source

pub open spec fn get_from_unused_perm_spec<M: AnyFrameMeta + Repr<MetaSlotStorage>>( paddr: Paddr, metadata: M, as_unique: bool, ptr: PPtr<MetaSlot>, perm: PointsTo<MetaSlot, Metadata<M>>, ) -> bool

{
    &&& ptr.addr() == frame_to_meta(paddr)
    &&& perm.addr() == frame_to_meta(paddr)
    &&& MetaSlot::get_from_unused_inner_perms_spec(as_unique, perm.inner_perms)

}
Source

pub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool

{ rc_perm.value() >= REF_COUNT_MAX }
Source

pub open spec fn frame_paddr_safety_cond(perm: PointsTo<MetaSlot>) -> bool

{
    &&& FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end
    &&& perm.addr() % META_SLOT_SIZE == 0

}
Source

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

{
    let idx = frame_to_index(paddr);
    let pre_perms = regions.slot_owners[idx].inner_perms.ref_count.value();
    pre_perms + 1 >= REF_COUNT_MAX
}
Source

pub open spec fn get_from_in_use_success( paddr: Paddr, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool

recommends
paddr % PAGE_SIZE == 0,
paddr < MAX_PADDR,
pre.inv(),
{
    let idx = frame_to_index(paddr);
    let pre_perms = pre.slot_owners[idx].inner_perms.ref_count.value();
    {
        &&& post.slot_owners[idx].inner_perms.ref_count.value() == pre_perms + 1
        &&& post.slot_owners[idx].inner_perms.ref_count.id()
            == pre.slot_owners[idx].inner_perms.ref_count.id()
        &&& post.slot_owners[idx].inner_perms.storage
            == pre.slot_owners[idx].inner_perms.storage
        &&& post.slot_owners[idx].inner_perms.vtable_ptr
            == pre.slot_owners[idx].inner_perms.vtable_ptr
        &&& post.slot_owners[idx].inner_perms.in_list
            == pre.slot_owners[idx].inner_perms.in_list
        &&& post.slot_owners[idx].self_addr == pre.slot_owners[idx].self_addr
        &&& post.slot_owners[idx].usage == pre.slot_owners[idx].usage
        &&& post.slot_owners[idx].raw_count == pre.slot_owners[idx].raw_count
        &&& post.slot_owners[idx].path_if_in_pt == pre.slot_owners[idx].path_if_in_pt
        &&& forall |i: usize| {
            i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
        }

    }
}
Source

pub open spec fn drop_last_in_place_safety_cond(owner: MetaSlotOwner) -> bool

{
    &&& (owner.inner_perms.ref_count.value() == 0
        || owner.inner_perms.ref_count.value() == REF_COUNT_UNIQUE)
    &&& owner.inner_perms.storage.is_init()
    &&& owner.inner_perms.in_list.value() == 0
    &&& owner.raw_count == 0

}
Source

pub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> MetaSlotModel

recommends
pre.inv(),
pre.status == MetaSlotStatus::SHARED,
{
    MetaSlotModel {
        ref_count: (pre.ref_count + 1) as u64,
        ..pre
    }
}

Trait Implementations§

Source§

impl ModelOf for MetaSlot

§

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

Source§

impl OwnerOf for MetaSlot

Source§

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

{
    &&& self.storage.id() == owner.inner_perms.storage.id()
    &&& self.ref_count.id() == owner.inner_perms.ref_count.id()
    &&& self.vtable_ptr == owner.inner_perms.vtable_ptr.pptr()
    &&& self.in_list.id() == owner.inner_perms.in_list.id()

}
Source§

type Owner = MetaSlotOwner

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>> Repr<MetaSlot> for Metadata<M>

Source§

open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool

{
    &&& perm.storage.id() == r.storage.id()
    &&& perm.ref_count.id() == r.ref_count.id()
    &&& perm.vtable_ptr.pptr() == r.vtable_ptr
    &&& perm.in_list.id() == r.in_list.id()

}
Source§

uninterp fn to_repr_spec( self, perm: MetadataInnerPerms, ) -> (MetaSlot, MetadataInnerPerms)

Source§

exec fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot

Source§

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

{
    Metadata {
        metadata: Self::metadata_from_inner_perms(perm.storage),
        ref_count: perm.ref_count.value(),
        vtable_ptr: perm.vtable_ptr.mem_contents(),
        in_list: perm.in_list.value(),
    }
}
Source§

exec fn from_repr(r: MetaSlot, Tracked(perm): Tracked<&MetadataInnerPerms>) -> Self

Source§

exec fn from_borrowed<'a>( r: &'a MetaSlot, verus_tmp_perm: Tracked<&'a MetadataInnerPerms>, ) -> &'a Self

Source§

proof fn from_to_repr(self, perm: MetadataInnerPerms)

Source§

proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms)

Source§

proof fn to_repr_wf(self, perm: MetadataInnerPerms)

Source§

type Perm = MetadataInnerPerms

If the underlying representation contains cells, the translation may require permission objects that access them.
Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlot> for MetadataAsLink<M>

Source§

uninterp fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool

Source§

uninterp fn to_repr_spec( self, perm: MetadataInnerPerms, ) -> (MetaSlot, MetadataInnerPerms)

Source§

exec fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot

Source§

uninterp fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self

Source§

exec fn from_repr(r: MetaSlot, Tracked(perm): Tracked<&MetadataInnerPerms>) -> Self

Source§

exec fn from_borrowed<'a>( r: &'a MetaSlot, verus_tmp_perm: Tracked<&'a MetadataInnerPerms>, ) -> &'a Self

Source§

proof fn from_to_repr(self, perm: MetadataInnerPerms)

Source§

proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms)

Source§

proof fn to_repr_wf(self, perm: MetadataInnerPerms)

Source§

type Perm = MetadataInnerPerms

If the underlying representation contains cells, the translation may require permission objects that access them.

Auto Trait Implementations§

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