#[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 MetaSlotto a*const AnyFrameMetafor manipulation; - if the metadata need special alignment, we can provide
at most
PAGE_METADATA_ALIGNbytes 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: PAtomicU64The 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 aUniqueFrame.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: PAtomicU64This 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
impl MetaSlot
Sourcepub proof fn lemma_layout()
pub proof fn lemma_layout()
core::mem::size_of::<MetaSlot>() == META_SLOT_SIZE,vstd::layout::size_of::<MetaSlot>() == META_SLOT_SIZE,Sourcepub exec fn cast_slot<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
&self,
addr: usize,
) -> res : ReprPtr<MetaSlot, Metadata<M>>
pub exec fn cast_slot<M: AnyFrameMeta + Repr<MetaSlotStorage>>( &self, addr: usize, ) -> res : ReprPtr<MetaSlot, Metadata<M>>
Tracked(perm): Tracked<&vstd::simple_pptr::PointsTo<MetaSlot>>,perm.value() == self,addr == perm.addr(),res.ptr.addr() == addr,res.addr() == addr,A helper function that casts a MetaSlot pointer to a Metadata pointer of type M.
Sourcepub open spec fn get_from_unused_inner_perms_spec(
as_unique: bool,
perms: MetadataInnerPerms,
) -> bool
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()
}Sourcepub open spec fn get_from_unused_spec(
paddr: Paddr,
as_unique: bool,
pre: MetaRegionOwners,
post: MetaRegionOwners,
) -> bool
pub open spec fn get_from_unused_spec( paddr: Paddr, as_unique: bool, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool
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].slot_vaddr == pre.slot_owners[idx].slot_vaddr
&&& 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).
Sourcepub open spec fn get_node_from_unused_spec(
paddr: Paddr,
pre: MetaRegionOwners,
post: MetaRegionOwners,
) -> bool
pub open spec fn get_node_from_unused_spec( paddr: Paddr, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool
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(
false,
post.slot_owners[idx].inner_perms,
)
&&& post.slot_owners[idx].usage == PageUsage::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: usize| {
i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
}
&&& pre.slot_owners[idx].inner_perms.ref_count.value() == 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).
Sourcepub open spec fn slot_perm_extracted_spec(
paddr: Paddr,
pre: MetaRegionOwners,
post: MetaRegionOwners,
) -> bool
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.
Sourcepub open spec fn slot_perm_reparked_spec(
paddr: Paddr,
pre: MetaRegionOwners,
post: MetaRegionOwners,
) -> bool
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.
Sourcepub open spec fn live_frame_obligations_ok_spec(
paddr: Paddr,
pre: MetaRegionOwners,
post: MetaRegionOwners,
) -> bool
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.
Sourcepub open spec fn live_frame_obligations_err_spec(
pre: MetaRegionOwners,
post: MetaRegionOwners,
) -> bool
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.
Sourcepub 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
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
}Sourcepub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool
pub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool
{ rc_perm.value() >= REF_COUNT_MAX }Sourcepub open spec fn frame_paddr_safety_cond(perm: PointsTo<MetaSlot>) -> bool
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
}Sourcepub open spec fn get_from_in_use_success(
paddr: Paddr,
pre: MetaRegionOwners,
post: MetaRegionOwners,
) -> bool
pub open spec fn get_from_in_use_success( paddr: Paddr, pre: MetaRegionOwners, post: MetaRegionOwners, ) -> bool
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].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: usize| {
i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
}
}
}Sourcepub open spec fn drop_last_in_place_safety_cond(owner: MetaSlotOwner) -> bool
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()
}Sourcepub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> MetaSlotModel
pub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> MetaSlotModel
pre.inv(),pre.status == MetaSlotStatus::SHARED,{
MetaSlotModel {
ref_count: (pre.ref_count + 1) as u64,
..pre
}
}Trait Implementations§
Source§impl OwnerOf for MetaSlot
impl OwnerOf for MetaSlot
Source§open spec fn wf(self, owner: Self::Owner) -> bool
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
type Owner = MetaSlotOwner
Inv, indicating that it must
has a consistent state.Source§impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M>
impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M>
Source§open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool
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)
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
exec fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot
Source§open spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self
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
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
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)
proof fn from_to_repr(self, perm: MetadataInnerPerms)
Source§proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms)
proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms)
Source§proof fn to_repr_wf(self, perm: MetadataInnerPerms)
proof fn to_repr_wf(self, perm: MetadataInnerPerms)
Source§type Perm = MetadataInnerPerms
type Perm = MetadataInnerPerms
Source§impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlot> for MetadataAsLink<M>
impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlot> for MetadataAsLink<M>
Source§open spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool
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)
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
exec fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot
Source§open spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self
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))
}