Skip to main content

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, ) -> res : ReprPtr<MetaSlot, Metadata<M>>

with
Tracked(perm): Tracked<&vstd::simple_pptr::PointsTo<MetaSlot>>,
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 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.slot_owners.dom() =~= pre.slot_owners.dom()
        &&& 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].self_addr == pre.slot_owners[idx].self_addr
        &&& post.slot_owners[idx].paths_in_pt == pre.slot_owners[idx].paths_in_pt
        &&& forall |i: usize| {
            i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
        }
        &&& pre.slot_owners[idx].inner_perms.ref_count.value() == REF_COUNT_UNUSED

    }
}

The slot_owners/obligations transition of claiming an unused slot, agnostic to where the extracted slot perm ends up. Says nothing about regions.slots — callers pin the permission location separately with [slot_perm_extracted_spec] (perm handed out, slot removed) or [slot_perm_reparked_spec] (perm re-parked, domain preserved).

Source

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

{ post.slots =~= pre.slots.remove(frame_to_index(paddr)) }

Permission-location clause: the slot perm was extracted (handed back to the caller via an out-param), so regions.slots loses it. Pairs with [get_from_unused_spec] to describe crate::mm::frame::MetaSlot::get_from_unused.

Source

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

{
    let idx = frame_to_index(paddr);
    &&& post.slots.dom() =~= pre.slots.dom()
    &&& forall |k: usize| {
        k != idx && pre.slots.contains_key(k) ==> post.slots[k] == pre.slots[k]
    }

}

Permission-location clause: the extracted slot perm was re-parked into regions.slots, so the domain is preserved and every other slot’s perm is untouched. Callers that re-park (see crate::mm::frame::Frame::from_unused — it hands the perm back via the perm out-param and re-inserts it) pair this with [get_from_unused_spec] (the slot_owners transition) to fully describe the Design-B post-state.

Source

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

{
    &&& post.frame_obligations =~= pre.frame_obligations.insert(frame_to_index(paddr))

}

Obligation-ledger effect of producing a fresh live Frame handle on success (e.g. crate::mm::frame::Frame::from_unused or crate::mm::frame::Frame::from_in_use): the segment obligations ledger is untouched, and the new handle mints its pending-Drop entry in frame_obligations at paddr.

Source

pub open spec fn live_frame_obligations_err_spec( pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool

{
    &&& post.frame_obligations =~= pre.frame_obligations

}

Obligation-ledger effect on failure: both the segment and frame ledgers are left untouched.

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

{
    &&& ptr.addr() == frame_to_meta(paddr)
    &&& perm.addr() == frame_to_meta(paddr)
    &&& perm.is_init()
    &&& perm.pptr() == ptr

}
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].paths_in_pt == pre.slot_owners[idx].paths_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.paths_in_pt.is_empty()

}
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§

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

{
    let new_perm = MetadataInnerPerms {
        storage: Self::inner_perms_from_metadata(self.metadata, perm.storage),
        ref_count: perm_u64_with(perm.ref_count, self.ref_count),
        vtable_ptr: pptr_usize_with(perm.vtable_ptr, self.vtable_ptr),
        in_list: perm_u64_with(perm.in_list, self.in_list),
    };
    (meta_slot_from_perm(new_perm), new_perm)
}
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§

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

{
    &&& <Metadata<Link<M>> as Repr<MetaSlot>>::wf(r, perm)

}
Source§

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

{
    <Metadata<
        Link<M>,
    > as Repr<
        MetaSlot,
    >>::to_repr_spec(
        <Metadata<Link<M>> as FromSpec<MetadataAsLink<M>>>::from_spec(self),
        perm,
    )
}
Source§

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

Source§

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

{
    <MetadataAsLink<
        M,
    > as FromSpec<
        Metadata<Link<M>>,
    >>::from_spec(<Metadata<Link<M>> as Repr<MetaSlot>>::from_repr_spec(r, perm))
}
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>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A