pub struct MetaRegionOwners {
pub slots: Map<usize, PointsTo<MetaSlot>>,
pub slot_owners: Map<usize, MetaSlotOwner>,
pub frame_obligations: Multiset<usize>,
}Expand description
Represents the ownership of the meta-frame memory region.
§Verification Design
§Slot owners
Every metadata slot has its owner (MetaSlotOwner) tracked by the slot_owners map at all times.
This makes the MetaRegionOwners the one place that tracks every frame, whether or not it is
in use.
§Slot permissions
We treat the slot permissions differently depending on how they are used. The permissions of unused slots
are tracked in slots, as are those of frames that do not otherwise belong to any other data structure.
This is necessary because those frames can have a new reference taken at any time via Frame::from_in_use.
Unique frames and frames that are forgotten with into_raw have their permissions tracked by the owner of
whatever object they belong to. Their permissions will be returned to slots when the object is dropped.
Whether or not the frame has a permission in slots, it will always have an owner in slot_owners,
which tracks information that needs to be globally visible.
§Safety
Forgetting a slot with into_raw or ManuallyDrop::new will leak the frame.
Forgetting it multiple times without restoring it will likely result in a memory leak, but not double-free.
Double-free happens when from_raw is called on a frame that is not forgotten, or that has been
dropped with ManuallyDrop::drop instead of into_raw. All functions in
the verified code that call from_raw have a precondition that the frame’s index is not a key in slots.
Fields§
§slots: Map<usize, PointsTo<MetaSlot>>§slot_owners: Map<usize, MetaSlotOwner>§frame_obligations: Multiset<usize>Outstanding per-instance obligations for both Frame<M> and
Segment<M>, as a multiset of slot indices. ManuallyDrop::new(frame, ..) adds one entry at frame.key() (mint paired with the raw_count++
bump); Frame::drop (via consume_obligation) and ManuallyDrop::new
redeem one. A Segment<M> records one entry per frame it holds (see
crate::specs::mm::frame::segment::tracked_mint_seg_obligations).
Multiset semantics — multiple outstanding obligations at the same slot
are counted individually.
Implementations§
Source§impl MetaRegionOwners
impl MetaRegionOwners
Sourcepub open spec fn ref_count(self, i: usize) -> res : u64
pub open spec fn ref_count(self, i: usize) -> res : u64
self.inv(),i < max_meta_slots() as usize,{ self.slot_owners[i].inner_perms.ref_count.value() }Sourcepub open spec fn slot_owners_agree_except(
self,
other: MetaRegionOwners,
idx: usize,
) -> bool
pub open spec fn slot_owners_agree_except( self, other: MetaRegionOwners, idx: usize, ) -> bool
{ forall |i: usize| i != idx ==> other.slot_owners[i] == self.slot_owners[i] }other agrees with self on every slot owner except the one at index
idx: a single-slot operation leaves all other slots’ owners untouched.
Sourcepub proof fn borrow_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
&self,
i: usize,
) -> tracked res : &PointsTo<MetaSlot, Metadata<M>>
pub proof fn borrow_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>( &self, i: usize, ) -> tracked res : &PointsTo<MetaSlot, Metadata<M>>
self.slots.contains_key(i),self.slot_owners.contains_key(i),vstd_extra::cast_ptr::PointsTo::<
MetaSlot,
Metadata<M>,
>::new_spec(self.slots[i], self.slot_owners[i].inner_perms)
.wf(&self.slot_owners[i].inner_perms),res.points_to == self.slots[i],res.inner_perms == self.slot_owners[i].inner_perms,res.wf(&res.inner_perms),Sourcepub proof fn borrow_mut_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
&mut self,
i: usize,
) -> tracked res : &mut PointsTo<MetaSlot, Metadata<M>>
pub proof fn borrow_mut_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>( &mut self, i: usize, ) -> tracked res : &mut PointsTo<MetaSlot, Metadata<M>>
old(self).slots.contains_key(i),old(self).slot_owners.contains_key(i),vstd_extra::cast_ptr::PointsTo::<
MetaSlot,
Metadata<M>,
>::new_spec(old(self).slots[i], old(self).slot_owners[i].inner_perms)
.wf(&old(self).slot_owners[i].inner_perms),res.points_to == old(self).slots[i],res.inner_perms == old(self).slot_owners[i].inner_perms,res.wf(&res.inner_perms),final(self).slots.dom() == old(self).slots.dom(),final(self).slot_owners.dom() == old(self).slot_owners.dom(),final(self).slots[i] == final(res).points_to,final(self).slot_owners[i].inner_perms == final(res).inner_perms,forall |k: usize| k != i ==> #[trigger] final(self).slots[k] == old(self).slots[k],forall |k: usize| {
k != i ==> #[trigger] final(self).slot_owners[k] == old(self).slot_owners[k]
},final(self).slot_owners[i].usage == old(self).slot_owners[i].usage,final(self).slot_owners[i].self_addr == old(self).slot_owners[i].self_addr,final(self).slot_owners[i].paths_in_pt == old(self).slot_owners[i].paths_in_pt,final(self).frame_obligations =~= old(self).frame_obligations,Mutable analog of [borrow_typed_perm]. Lends out a &'a mut cast_ptr
reconstructed from slots[i] (outer simple-pptr) and
slot_owners[i].inner_perms (inner perms). While the returned reference
is live, self is mutably borrowed; on borrow-end, self.slots[i] and
self.slot_owners[i].inner_perms are restored from the final cast_ptr.
Every other slot/slot_owner is fully preserved, and the other fields of
slot_owners[i] (raw_count/usage/self_addr/paths_in_pt) are unchanged.
Sourcepub open spec fn paddr_range_in_region(self, range: Range<Paddr>) -> bool
pub open spec fn paddr_range_in_region(self, range: Range<Paddr>) -> bool
self.inv(),range.start < range.end < MAX_PADDR,{
forall |paddr: Paddr| {
(range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
==> self.slots.contains_key(frame_to_index(paddr))
}
}Sourcepub open spec fn paddr_range_not_mapped(self, range: Range<Paddr>) -> bool
pub open spec fn paddr_range_not_mapped(self, range: Range<Paddr>) -> bool
self.inv(),range.start < range.end < MAX_PADDR,{
forall |paddr: Paddr| {
(range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
==> self.slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty()
}
}Sourcepub open spec fn paddr_range_not_in_region(self, range: Range<Paddr>) -> bool
pub open spec fn paddr_range_not_in_region(self, range: Range<Paddr>) -> bool
self.inv(),range.start < range.end < MAX_PADDR,{
forall |paddr: Paddr| {
(range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
==> !self.slots.contains_key(frame_to_index(paddr))
}
}Sourcepub proof fn paddr_not_mapped_at(self, range: Range<Paddr>, paddr: Paddr)
pub proof fn paddr_not_mapped_at(self, range: Range<Paddr>, paddr: Paddr)
self.paddr_range_not_mapped(range),range.start <= paddr,paddr < range.end,paddr % PAGE_SIZE == 0,self.slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),Instantiates paddr_range_not_mapped at a specific paddr in the range.
Sourcepub proof fn inv_implies_correct_addr(self, paddr: usize)
pub proof fn inv_implies_correct_addr(self, paddr: usize)
paddr < MAX_PADDR,paddr % PAGE_SIZE == 0,self.inv(),self.slot_owners.contains_key(frame_to_index(paddr) as usize),Sourcepub proof fn copy_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(tracked
&mut self,
index: usize,
) -> tracked perm : MetaPerm<M>
pub proof fn copy_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(tracked &mut self, index: usize, ) -> tracked perm : MetaPerm<M>
old(self).slots.contains_key(index),perm.points_to == old(self).slots[index],final(self).slots == old(self).slots.remove(index),final(self).slot_owners == old(self).slot_owners,final(self).frame_obligations =~= old(self).frame_obligations,Sourcepub proof fn sync_slot_perm(tracked &mut self, index: usize, perm: &PointsTo<MetaSlot>)
pub proof fn sync_slot_perm(tracked &mut self, index: usize, perm: &PointsTo<MetaSlot>)
final(self).slots == old(self).slots.insert(index, *perm),final(self).slot_owners == old(self).slot_owners,final(self).frame_obligations =~= old(self).frame_obligations,Move a slot pointer permission into slots[index] from caller-supplied storage.
Used by Frame::from_raw after the migration to typed slot perms — the perm being
returned to regions.slots has no inner_perms baggage; the inner-perms live in
slot_owners[index].inner_perms.
Sourcepub open spec fn clean_inv(self) -> bool
pub open spec fn clean_inv(self) -> bool
{
&&& self.inv()
&&& self.frame_obligations.len() == 0
}“Clean” boundary invariant: standard invariant plus an empty per-frame
obligation multiset (every minted token has been redeemed via
Drop::drop or ManuallyDrop::new; and every Segment has been
dropped, draining its per-frame entries).
Functions that should leave no outstanding Frame/Segment obligations
(e.g., top-of-call-stack entry points, or any helper that opens fresh
resources locally) should require this in their postcondition instead of
the plain inv().
Sourcepub proof fn tracked_mint_frame_obligation(tracked
&mut self,
slot_idx: usize,
) -> tracked obl : DropObligation<usize>
pub proof fn tracked_mint_frame_obligation(tracked &mut self, slot_idx: usize, ) -> tracked obl : DropObligation<usize>
obl.value() == slot_idx,final(self).frame_obligations =~= old(self).frame_obligations.insert(slot_idx),final(self).slots =~= old(self).slots,final(self).slot_owners =~= old(self).slot_owners,Pairs the production of a per-Frame [DropObligation] with a
+1 on the frame_obligations[slot_idx] count. Called by Frame’s
constructor_spec (i.e. ManuallyDrop::new(frame, ..)).
Sourcepub proof fn tracked_redeem_frame_obligation(tracked &mut self, tracked obl: DropObligation<usize>)
pub proof fn tracked_redeem_frame_obligation(tracked &mut self, tracked obl: DropObligation<usize>)
old(self).frame_obligations.count(obl.value()) > 0,final(self).frame_obligations =~= old(self).frame_obligations.remove(obl.value()),final(self).slots =~= old(self).slots,final(self).slot_owners =~= old(self).slot_owners,Redeems a per-Frame obligation, decrementing frame_obligations
at obl.value(). Called by Frame’s consume_obligation (i.e.
by Drop::drop or ManuallyDrop::new).
Trait Implementations§
Source§impl Inv for MetaRegionOwners
impl Inv for MetaRegionOwners
Source§open spec fn inv(self) -> bool
open spec fn inv(self) -> bool
{
&&& self.slots.dom().finite()
&&& {
forall |i: usize| {
i < max_meta_slots() <==> #[trigger] self.slot_owners.contains_key(i)
}
}
&&& {
forall |i: usize| {
#[trigger] self.slot_owners.contains_key(i) ==> self.slots.contains_key(i)
}
}
&&& {
forall |i: usize| #[trigger] self.slots.contains_key(i) ==> i < max_meta_slots()
}
&&& {
forall |i: usize| {
#[trigger] self.slots.contains_key(i)
==> {
&&& self.slot_owners.contains_key(i)
&&& self.slot_owners[i].inv()
&&& self.slots[i].is_init()
&&& self.slots[i].addr() == meta_addr(i)
&&& self.slots[i].value().wf(self.slot_owners[i])
&&& self.slot_owners.contains_key(i)
&&& self.slot_owners[i].self_addr == self.slots[i].addr()
}
}
}
&&& {
forall |i: usize| {
#[trigger] self.slot_owners.contains_key(i)
==> {
&&& self.slot_owners[i].inv()
}
}
}
}