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 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.storage_perm().is_init()
    &&& owner.vtable_ptr_perm().is_init()

}

pub open spec fn get_from_unused_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 slot_owners/obligations transition of claiming an unused slot.

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_spec] for allocating a page-table node (always non-unique). Identical except the claimed slot becomes PageUsage::PageTable rather than PageUsage::Frame: a page-table node is tracked with PageTable usage, which gives a clean usage-based discriminator between node slots and data-frame slots (the latter are Frame/MMIO). Used by the node allocators (PageTableNode::alloc, PageTable::empty_with_owner).

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

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.

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.

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

}

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( paddr: Paddr, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool

{
    let idx = frame_to_index(paddr);
    let pre_perms = pre.slot_owners[idx].ref_count();
    {
        &&& post.slot_owners[idx].ref_count() == pre_perms + 1
        &&& post.slot_owners[idx].ref_count_perm.id()
            == pre.slot_owners[idx].ref_count_perm.id()
        &&& post.slot_owners[idx].storage_perm() == pre.slot_owners[idx].storage_perm()
        &&& post.slot_owners[idx].vtable_ptr_perm()
            == pre.slot_owners[idx].vtable_ptr_perm()
        &&& post.slot_owners[idx].in_list_perm == pre.slot_owners[idx].in_list_perm
        &&& post.slot_owners[idx].slot_vaddr == pre.slot_owners[idx].slot_vaddr
        &&& 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: int| {
            i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
        }

    }
}

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

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

}

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

recommends

pre.status == MetaSlotStatus::SHARED,

{
    MetaSlotModel {
        ref_count: (pre.ref_count + 1) as u64,
        ..pre
    }
}

Trait Implementations

impl OwnerOf for MetaSlot

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

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

}

type Owner = MetaSlotOwner

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