ostd/specs/mm/frame/
meta_region_owners.rs

1use vstd::atomic::*;
2use vstd::cell;
3use vstd::prelude::*;
4use vstd::simple_pptr::{self, *};
5
6use core::ops::Range;
7
8use vstd_extra::cast_ptr::Repr;
9use vstd_extra::ghost_tree::TreePath;
10use vstd_extra::ownership::*;
11
12use super::meta_owners::{MetaPerm, MetaSlotModel, MetaSlotOwner, MetaSlotStorage};
13use super::*;
14use crate::mm::frame::meta::{
15    mapping::{frame_to_index_spec, frame_to_meta, max_meta_slots, meta_addr, META_SLOT_SIZE},
16    AnyFrameMeta, MetaSlot,
17};
18use crate::mm::Paddr;
19use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
20use crate::specs::arch::mm::{MAX_PADDR, NR_ENTRIES, PAGE_SIZE};
21
22verus! {
23
24/// Represents the meta-frame memory region. Can be viewed as a collection of
25/// Cell<MetaSlot> at a fixed address range.
26pub struct MetaRegion;
27
28/// Represents the ownership of the meta-frame memory region.
29/// # Verification Design
30/// ## Slot owners
31/// Every metadata slot has its owner ([`MetaSlotOwner`]) tracked by the `slot_owners` map at all times.
32/// This makes the `MetaRegionOwners` the one place that tracks every frame, whether or not it is
33/// in use.
34/// ## Slot permissions
35/// We treat the slot permissions differently depending on how they are used. The permissions of unused slots
36/// are tracked in `slots`, as are those of frames that do not otherwise belong to any other data structure.
37/// This is necessary because those frames can have a new reference taken at any time via `Frame::from_in_use`.
38/// Unique frames and frames that are forgotten with `into_raw` have their permissions tracked by the owner of
39/// whatever object they belong to. Their permissions will be returned to `slots` when the object is dropped.
40/// Whether or not the frame has a permission in `slots`, it will always have an owner in `slot_owners`,
41/// which tracks information that needs to be globally visible.
42/// ## Safety
43/// Forgetting a slot with `into_raw` or `ManuallyDrop::new` will leak the frame.
44/// Forgetting it multiple times without restoring it will likely result in a memory leak, but not double-free.
45/// Double-free happens when `from_raw` is called on a frame that is not forgotten, or that has been
46/// dropped with `ManuallyDrop::drop` instead of `into_raw`. All functions in
47/// the verified code that call `from_raw` have a precondition that the frame's index is not a key in `slots`.
48pub tracked struct MetaRegionOwners {
49    pub slots: Map<usize, simple_pptr::PointsTo<MetaSlot>>,
50    pub slot_owners: Map<usize, MetaSlotOwner>,
51}
52
53pub ghost struct MetaRegionModel {
54    pub slots: Map<usize, MetaSlotModel>,
55}
56
57impl Inv for MetaRegionOwners {
58    open spec fn inv(self) -> bool {
59        &&& self.slots.dom().finite()
60        &&& {
61            // All accessible slots are within the valid address range.
62            forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slot_owners.contains_key(i)
63        }
64        &&& { forall|i: usize| #[trigger] self.slots.contains_key(i) ==> i < max_meta_slots() }
65        &&& {
66            forall|i: usize| #[trigger]
67                self.slots.contains_key(i) ==> {
68                    &&& self.slot_owners.contains_key(i)
69                    &&& self.slot_owners[i].inv()
70                    &&& self.slots[i].is_init()
71                    &&& self.slots[i].addr() == meta_addr(i)
72                    &&& self.slots[i].value().wf(self.slot_owners[i])
73                    &&& self.slot_owners.contains_key(i)
74                    &&& self.slot_owners[i].self_addr == self.slots[i].addr()
75                }
76        }
77        &&& {
78            forall|i: usize| #[trigger]
79                self.slot_owners.contains_key(i) ==> {
80                    &&& self.slot_owners[i].inv()
81                }
82        }
83    }
84}
85
86impl Inv for MetaRegionModel {
87    open spec fn inv(self) -> bool {
88        &&& self.slots.dom().finite()
89        &&& forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slots.contains_key(i)
90        &&& forall|i: usize| #[trigger] self.slots.contains_key(i) ==> self.slots[i].inv()
91    }
92}
93
94impl View for MetaRegionOwners {
95    type V = MetaRegionModel;
96
97    open spec fn view(&self) -> <Self as View>::V {
98        let slots = self.slot_owners.map_values(|s: MetaSlotOwner| s@);
99        MetaRegionModel { slots }
100    }
101}
102
103impl InvView for MetaRegionOwners {
104    // XXX: verus `map_values` does not preserves the `finite()` attribute.
105    axiom fn view_preserves_inv(self);
106}
107
108impl OwnerOf for MetaRegion {
109    type Owner = MetaRegionOwners;
110
111    open spec fn wf(self, owner: Self::Owner) -> bool {
112        true
113    }
114}
115
116impl ModelOf for MetaRegion {
117
118}
119
120impl MetaRegionOwners {
121    pub open spec fn ref_count(self, i: usize) -> (res: u64)
122        recommends
123            self.inv(),
124            i < max_meta_slots() as usize,
125    {
126        self.slot_owners[i].inner_perms.ref_count.value()
127    }
128
129    pub open spec fn paddr_range_in_region(self, range: Range<Paddr>) -> bool
130        recommends
131            self.inv(),
132            range.start < range.end < MAX_PADDR,
133    {
134        forall|paddr: Paddr|
135            #![trigger frame_to_index_spec(paddr)]
136            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
137                ==> self.slots.contains_key(frame_to_index_spec(paddr))
138    }
139
140    pub open spec fn paddr_range_not_mapped(self, range: Range<Paddr>) -> bool
141        recommends
142            self.inv(),
143            range.start < range.end < MAX_PADDR,
144    {
145        forall|paddr: Paddr|
146            #![trigger frame_to_index_spec(paddr)]
147            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
148                ==> self.slot_owners[frame_to_index_spec(paddr)].path_if_in_pt is None
149    }
150
151    pub open spec fn paddr_range_not_in_region(self, range: Range<Paddr>) -> bool
152        recommends
153            self.inv(),
154            range.start < range.end < MAX_PADDR,
155    {
156        forall|paddr: Paddr|
157            #![trigger frame_to_index_spec(paddr)]
158            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
159                ==> !self.slots.contains_key(frame_to_index_spec(paddr))
160    }
161
162    pub proof fn inv_implies_correct_addr(self, paddr: usize)
163        requires
164            paddr < MAX_PADDR,
165            paddr % PAGE_SIZE == 0,
166            self.inv(),
167        ensures
168            self.slot_owners.contains_key(frame_to_index_spec(paddr) as usize),
169    {
170        assert((frame_to_index_spec(paddr)) < max_meta_slots() as usize);
171    }
172
173    pub axiom fn sync_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
174        tracked &mut self,
175        index: usize,
176        perm: &MetaPerm<M>,
177    )
178        ensures
179            self.slots == old(self).slots.insert(index, perm.points_to),
180            self.slot_owners == old(self).slot_owners;
181
182    pub axiom fn copy_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
183        tracked &mut self,
184        index: usize,
185    ) -> (tracked perm: MetaPerm<M>)
186        requires
187            old(self).slots.contains_key(index),
188        ensures
189            perm.points_to == old(self).slots[index],
190            self.slots == old(self).slots.remove(index),
191            self.slot_owners == old(self).slot_owners;
192}
193
194} // verus!
ostd/specs/mm/frame/meta_region_owners.rs

ostd/specs/mm/frame/
meta_region_owners.rs
