pub struct MetaRegionOwners {
pub slots: Map<usize, PointsTo<MetaSlot>>,
pub slot_owners: Map<usize, MetaSlotOwner>,
}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>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 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_spec(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_spec(paddr)].path_if_in_pt is None
}
}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_spec(paddr))
}
}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_spec(paddr) as usize),Sourcepub proof fn sync_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(tracked
&mut self,
index: usize,
perm: &MetaPerm<M>,
)
pub proof fn sync_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(tracked &mut self, index: usize, perm: &MetaPerm<M>, )
self.slots == old(self).slots.insert(index, perm.points_to),self.slot_owners == old(self).slot_owners,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],self.slots == old(self).slots.remove(index),self.slot_owners == old(self).slot_owners,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.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()
}
}
}
}