Struct MetaSlot 

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

Don’t interpret this field as an array of bytes. It is a placeholder for the metadata of a frame.

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. VERUS LIMITATION: 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

impl MetaSlot

pub open spec fn perms_related( slot_perm: PointsTo<MetaSlot>, metadata_perm: MetadataPerm, ) -> bool

{
    &&& metadata_perm.storage_perm.is_init()
    &&& metadata_perm.vtable_ptr_perm.is_init()
    &&& slot_perm.value().storage.id() == metadata_perm.storage_perm.id()
    &&& slot_perm.value().vtable_ptr == metadata_perm.vtable_ptr_perm.pptr()

}

The relation between the MetaSlot permission and a metadata permission fraction.

pub proof fn lemma_layout()

ensures

core::mem::size_of::<MetaSlot>() == META_SLOT_SIZE,

vstd::layout::size_of::<MetaSlot>() == META_SLOT_SIZE,

pub open spec fn get_from_unused_owner_spec(as_unique: bool, owner: MetaSlotOwner) -> bool

{
    &&& owner.ref_count() == (if as_unique { REF_COUNT_UNIQUE as u64 } else { 1u64 })
    &&& owner.in_list_perm.value() == 0
    &&& owner.metadata_perm.frac() == (if as_unique { 0int } else { REF_COUNT_MAX - 1 })
    &&& as_unique ==> owner.metadata_perm.is_resource_vacant()
    &&& !as_unique
        ==> {
            &&& owner.storage_perm().is_init()
            &&& owner.vtable_ptr_perm().is_init()

        }

}

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

{
    let idx = frame_to_index(paddr);
    let pre_owner = pre.slot_owners[idx];
    let post_owner = post.slot_owners[idx];
    {
        &&& pre_owner.ref_count() == REF_COUNT_UNUSED
        &&& MetaSlot::get_from_unused_owner_spec(as_unique, post_owner)
        &&& post_owner.usage is Frame
        &&& post_owner.slot_vaddr == pre_owner.slot_vaddr
        &&& post_owner.paths_in_pt == pre_owner.paths_in_pt
        &&& post =~= pre.insert_slot_owner(paddr, post_owner)

    }
}

The metadata region transition of claiming an unused slot.

pub open spec fn get_from_unused_spec<M: AnyFrameMeta + Repr<MetaSlotStorage>>( paddr: Paddr, metadata: M, as_unique: bool, pre: MetaRegionOwners, post: MetaRegionOwners, repr_perm: M::ReprPerm, permission: Sum<FracMetadataPerm, MetadataPerm>, ) -> bool

{
    let idx = frame_to_index(paddr);
    let metadata_perms = match permission {
        Sum::Left(permission) => permission.resource(),
        Sum::Right(permission) => permission,
    };
    &&& Self::get_from_unused_region_spec(paddr, as_unique, pre, post)
    &&& as_unique ==> permission is Right
    &&& !as_unique
        ==> {
            &&& permission is Left
            &&& permission->Left_0.frac() == 1
            &&& permission->Left_0.id() == post.slot_owners[idx].metadata_perm.id()

        }
    &&& Self::perms_related(*post.slots[idx], metadata_perms)
    &&& <M as Repr<MetaSlotStorage>>::wf(metadata_perms.storage_perm.value(), repr_perm)
    &&& M::from_repr_spec(metadata_perms.storage_perm.value(), repr_perm) == metadata

}

The complete successful result of claiming an unused slot, including the fraction returned to the new frame handle.

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

{
    let idx = frame_to_index(paddr);
    {
        &&& post.slot_owners.dom() =~= pre.slot_owners.dom()
        &&& MetaSlot::get_from_unused_owner_spec(false, post.slot_owners[idx])
        &&& post.slot_owners[idx].usage is PageTable
        &&& post.slot_owners[idx].slot_vaddr == pre.slot_owners[idx].slot_vaddr
        &&& post.slot_owners[idx].paths_in_pt == pre.slot_owners[idx].paths_in_pt
        &&& forall |i: int| {
            i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
        }
        &&& pre.slot_owners[idx].ref_count() == REF_COUNT_UNUSED

    }
}

Variant of [get_from_unused_region_spec] for allocating a page-table node (always non-unique). Identical except the claimed slot becomes PageUsage::PageTable rather than PageUsage::Frame.

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: int| k != idx && pre.contains(k) ==> post.slots[k] == pre.slots[k]

}

Permission-location clause for the static MetaSlot permissions. Only the slot at paddr is changed.

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

{ rc_perm.value() >= REF_COUNT_MAX }

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

}

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

{
    let idx = frame_to_index(paddr);
    {
        &&& pre.inc_frame_reference_region_spec(paddr, post)
        &&& metadata_perm.frac() == 1
        &&& metadata_perm.id() == post.slot_owners[idx].metadata_perm.id()
        &&& Self::perms_related(*post.slots[idx], metadata_perm.resource())

    }
}

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

{
    &&& (owner.ref_count() == 0 || owner.ref_count() == REF_COUNT_UNIQUE)
    &&& owner.metadata_perm.is_full()
    &&& owner.storage_perm().is_init()
    &&& owner.vtable_ptr_perm().is_init()
    &&& owner.in_list_perm.value() == 0
    &&& owner.paths_in_pt.is_empty()

}

Trait Implementations

impl OwnerOf for MetaSlot

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

{
    &&& self.ref_count.id() == owner.ref_count_perm.id()
    &&& self.in_list.id() == owner.in_list_perm.id()
    &&& owner.metadata_perm.not_empty()
        ==> {
            &&& self.storage.id() == owner.storage_perm().id()
            &&& self.vtable_ptr == owner.vtable_ptr_perm().pptr()

        }

}

type Owner = MetaSlotOwner

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