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::{self, Repr};
9use vstd_extra::drop_tracking::DropObligation;
10use vstd_extra::ghost_tree::TreePath;
11use vstd_extra::ownership::*;
12
13use super::meta_owners::{MetaPerm, MetaSlotModel, MetaSlotOwner, MetaSlotStorage};
14use super::*;
15use crate::mm::Paddr;
16use crate::mm::frame::Link;
17use crate::mm::frame::meta::{
18    AnyFrameMeta, MetaSlot, REF_COUNT_MAX,
19    mapping::{META_SLOT_SIZE, frame_to_index, frame_to_meta, max_meta_slots, meta_addr},
20};
21use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
22use crate::specs::arch::mm::{MAX_PADDR, NR_ENTRIES, PAGE_SIZE};
23use crate::specs::mm::frame::linked_list::linked_list_owners::MetaSlotSmall;
24use crate::specs::mm::frame::meta_owners::Metadata;
25
26verus! {
27
28/// Represents the meta-frame memory region. Can be viewed as a collection of
29/// Cell<MetaSlot> at a fixed address range.
30pub struct MetaRegion;
31
32/// Represents the ownership of the meta-frame memory region.
33/// # Verification Design
34/// ## Slot owners
35/// Every metadata slot has its owner ([`MetaSlotOwner`]) tracked by the `slot_owners` map at all times.
36/// This makes the `MetaRegionOwners` the one place that tracks every frame, whether or not it is
37/// in use.
38/// ## Slot permissions
39/// We treat the slot permissions differently depending on how they are used. The permissions of unused slots
40/// are tracked in `slots`, as are those of frames that do not otherwise belong to any other data structure.
41/// This is necessary because those frames can have a new reference taken at any time via `Frame::from_in_use`.
42/// Unique frames and frames that are forgotten with `into_raw` have their permissions tracked by the owner of
43/// whatever object they belong to. Their permissions will be returned to `slots` when the object is dropped.
44/// Whether or not the frame has a permission in `slots`, it will always have an owner in `slot_owners`,
45/// which tracks information that needs to be globally visible.
46/// ## Safety
47/// Forgetting a slot with `into_raw` or `ManuallyDrop::new` will leak the frame.
48/// Forgetting it multiple times without restoring it will likely result in a memory leak, but not double-free.
49/// Double-free happens when `from_raw` is called on a frame that is not forgotten, or that has been
50/// dropped with `ManuallyDrop::drop` instead of `into_raw`. All functions in
51/// the verified code that call `from_raw` have a precondition that the frame's index is not a key in `slots`.
52pub tracked struct MetaRegionOwners {
53    pub slots: Map<usize, simple_pptr::PointsTo<MetaSlot>>,
54    pub slot_owners: Map<usize, MetaSlotOwner>,
55    /// Outstanding per-instance obligations for both `Frame<M>` and
56    /// `Segment<M>`, as a multiset of slot indices. `ManuallyDrop::new(frame,
57    /// ..)` adds one entry at `frame.key()` (mint paired with the `raw_count++`
58    /// bump); `Frame::drop` (via `consume_obligation`) and `ManuallyDrop::new`
59    /// redeem one. A `Segment<M>` records one entry per frame it holds (see
60    /// [`crate::specs::mm::frame::segment::tracked_mint_seg_obligations`]).
61    /// Multiset semantics — multiple outstanding obligations at the same slot
62    /// are counted individually.
63    pub frame_obligations: vstd::multiset::Multiset<usize>,
64}
65
66pub ghost struct MetaRegionModel {
67    pub slots: Map<usize, MetaSlotModel>,
68}
69
70impl Inv for MetaRegionOwners {
71    open spec fn inv(self) -> bool {
72        &&& self.slots.dom().finite()
73        &&& {
74            // All accessible slots are within the valid address range.
75            forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slot_owners.contains_key(i)
76        }
77        &&& {
78            forall|i: usize| #[trigger]
79                self.slot_owners.contains_key(i) ==> self.slots.contains_key(i)
80        }
81        &&& { forall|i: usize| #[trigger] self.slots.contains_key(i) ==> i < max_meta_slots() }
82        &&& {
83            forall|i: usize| #[trigger]
84                self.slots.contains_key(i) ==> {
85                    &&& self.slot_owners.contains_key(i)
86                    &&& self.slot_owners[i].inv()
87                    &&& self.slots[i].is_init()
88                    &&& self.slots[i].addr() == meta_addr(i)
89                    &&& self.slots[i].value().wf(self.slot_owners[i])
90                    &&& self.slot_owners.contains_key(i)
91                    &&& self.slot_owners[i].self_addr == self.slots[i].addr()
92                }
93        }
94        &&& {
95            forall|i: usize| #[trigger]
96                self.slot_owners.contains_key(i) ==> {
97                    &&& self.slot_owners[i].inv()
98                }
99        }
100    }
101}
102
103impl Inv for MetaRegionModel {
104    open spec fn inv(self) -> bool {
105        &&& self.slots.dom().finite()
106        &&& forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slots.contains_key(i)
107        &&& forall|i: usize| #[trigger] self.slots.contains_key(i) ==> self.slots[i].inv()
108    }
109}
110
111impl View for MetaRegionOwners {
112    type V = MetaRegionModel;
113
114    open spec fn view(&self) -> <Self as View>::V {
115        let slots = self.slot_owners.map_values(|s: MetaSlotOwner| s@);
116        MetaRegionModel { slots }
117    }
118}
119
120impl InvView for MetaRegionOwners {
121    // XXX: verus `map_values` does not preserves the `finite()` attribute.
122    axiom fn view_preserves_inv(self);
123}
124
125impl OwnerOf for MetaRegion {
126    type Owner = MetaRegionOwners;
127
128    open spec fn wf(self, owner: Self::Owner) -> bool {
129        true
130    }
131}
132
133impl ModelOf for MetaRegion {
134
135}
136
137impl MetaRegionOwners {
138    pub open spec fn ref_count(self, i: usize) -> (res: u64)
139        recommends
140            self.inv(),
141            i < max_meta_slots() as usize,
142    {
143        self.slot_owners[i].inner_perms.ref_count.value()
144    }
145
146    /// `other` agrees with `self` on every slot owner except the one at index
147    /// `idx`: a single-slot operation leaves all other slots' owners untouched.
148    pub open spec fn slot_owners_agree_except(self, other: MetaRegionOwners, idx: usize) -> bool {
149        forall|i: usize|
150            #![trigger other.slot_owners[i]]
151            i != idx ==> other.slot_owners[i] == self.slot_owners[i]
152    }
153
154    pub axiom fn borrow_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
155        &self,
156        i: usize,
157    ) -> (tracked res: &vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<M>>)
158        requires
159            self.slots.contains_key(i),
160            self.slot_owners.contains_key(i),
161            vstd_extra::cast_ptr::PointsTo::<MetaSlot, Metadata<M>>::new_spec(
162                self.slots[i],
163                self.slot_owners[i].inner_perms,
164            ).wf(&self.slot_owners[i].inner_perms),
165        ensures
166            res.points_to == self.slots[i],
167            res.inner_perms == self.slot_owners[i].inner_perms,
168            res.wf(&res.inner_perms),
169    ;
170
171    /// Mutable analog of [`borrow_typed_perm`]. Lends out a `&'a mut cast_ptr`
172    /// reconstructed from `slots[i]` (outer simple-pptr) and
173    /// `slot_owners[i].inner_perms` (inner perms). While the returned reference
174    /// is live, `self` is mutably borrowed; on borrow-end, `self.slots[i]` and
175    /// `self.slot_owners[i].inner_perms` are restored from the final cast_ptr.
176    /// Every other slot/slot_owner is fully preserved, and the other fields of
177    /// `slot_owners[i]` (raw_count/usage/self_addr/paths_in_pt) are unchanged.
178    pub axiom fn borrow_mut_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
179        &mut self,
180        i: usize,
181    ) -> (tracked res: &mut vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<M>>)
182        requires
183            old(self).slots.contains_key(i),
184            old(self).slot_owners.contains_key(i),
185            vstd_extra::cast_ptr::PointsTo::<MetaSlot, Metadata<M>>::new_spec(
186                old(self).slots[i],
187                old(self).slot_owners[i].inner_perms,
188            ).wf(&old(self).slot_owners[i].inner_perms),
189        ensures
190            res.points_to == old(self).slots[i],
191            res.inner_perms == old(self).slot_owners[i].inner_perms,
192            res.wf(&res.inner_perms),
193            final(self).slots.dom() == old(self).slots.dom(),
194            final(self).slot_owners.dom() == old(self).slot_owners.dom(),
195            final(self).slots[i] == final(res).points_to,
196            final(self).slot_owners[i].inner_perms == final(res).inner_perms,
197            forall|k: usize| k != i ==> #[trigger] final(self).slots[k] == old(self).slots[k],
198            forall|k: usize|
199                k != i ==> #[trigger] final(self).slot_owners[k] == old(self).slot_owners[k],
200            final(self).slot_owners[i].usage == old(self).slot_owners[i].usage,
201            final(self).slot_owners[i].self_addr == old(self).slot_owners[i].self_addr,
202            final(self).slot_owners[i].paths_in_pt == old(self).slot_owners[i].paths_in_pt,
203            final(self).frame_obligations =~= old(self).frame_obligations,
204    ;
205
206    pub open spec fn paddr_range_in_region(self, range: Range<Paddr>) -> bool
207        recommends
208            self.inv(),
209            range.start < range.end < MAX_PADDR,
210    {
211        forall|paddr: Paddr|
212            #![trigger frame_to_index(paddr)]
213            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
214                ==> self.slots.contains_key(frame_to_index(paddr))
215    }
216
217    pub open spec fn paddr_range_not_mapped(self, range: Range<Paddr>) -> bool
218        recommends
219            self.inv(),
220            range.start < range.end < MAX_PADDR,
221    {
222        forall|paddr: Paddr|
223            #![trigger frame_to_index(paddr)]
224            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
225                ==> self.slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty()
226    }
227
228    pub open spec fn paddr_range_not_in_region(self, range: Range<Paddr>) -> bool
229        recommends
230            self.inv(),
231            range.start < range.end < MAX_PADDR,
232    {
233        forall|paddr: Paddr|
234            #![trigger frame_to_index(paddr)]
235            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
236                ==> !self.slots.contains_key(frame_to_index(paddr))
237    }
238
239    /// Instantiates `paddr_range_not_mapped` at a specific paddr in the range.
240    pub proof fn paddr_not_mapped_at(self, range: Range<Paddr>, paddr: Paddr)
241        requires
242            self.paddr_range_not_mapped(range),
243            range.start <= paddr,
244            paddr < range.end,
245            paddr % PAGE_SIZE == 0,
246        ensures
247            self.slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
248    {
249        // The trigger frame_to_index(paddr) fires from the ensures clause,
250        // instantiating the forall in paddr_range_not_mapped at this paddr.
251    }
252
253    pub proof fn inv_implies_correct_addr(self, paddr: usize)
254        requires
255            paddr < MAX_PADDR,
256            paddr % PAGE_SIZE == 0,
257            self.inv(),
258        ensures
259            self.slot_owners.contains_key(frame_to_index(paddr) as usize),
260    {
261        assert((frame_to_index(paddr)) < max_meta_slots() as usize);
262    }
263
264    pub axiom fn copy_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
265        tracked &mut self,
266        index: usize,
267    ) -> (tracked perm: MetaPerm<M>)
268        requires
269            old(self).slots.contains_key(index),
270        ensures
271            perm.points_to == old(self).slots[index],
272            final(self).slots == old(self).slots.remove(index),
273            final(self).slot_owners == old(self).slot_owners,
274            final(self).frame_obligations =~= old(self).frame_obligations,
275    ;
276
277    /// Move a slot pointer permission *into* `slots[index]` from caller-supplied storage.
278    /// Used by `Frame::from_raw` after the migration to typed slot perms — the perm being
279    /// returned to `regions.slots` has no `inner_perms` baggage; the inner-perms live in
280    /// `slot_owners[index].inner_perms`.
281    pub axiom fn sync_slot_perm(
282        tracked &mut self,
283        index: usize,
284        perm: &simple_pptr::PointsTo<MetaSlot>,
285    )
286        ensures
287            final(self).slots == old(self).slots.insert(index, *perm),
288            final(self).slot_owners == old(self).slot_owners,
289            final(self).frame_obligations =~= old(self).frame_obligations,
290    ;
291
292    // ----------------------------------------------------------------------
293    // Per-frame linear-drop ledger machinery.
294    // ----------------------------------------------------------------------
295    /// "Clean" boundary invariant: standard invariant plus an empty per-frame
296    /// obligation multiset (every minted token has been redeemed via
297    /// `Drop::drop` or `ManuallyDrop::new`; and every `Segment` has been
298    /// dropped, draining its per-frame entries).
299    ///
300    /// Functions that should leave no outstanding `Frame`/`Segment` obligations
301    /// (e.g., top-of-call-stack entry points, or any helper that opens fresh
302    /// resources locally) should require this in their postcondition instead of
303    /// the plain `inv()`.
304    pub open spec fn clean_inv(self) -> bool {
305        &&& self.inv()
306        // Per-frame linear-drop discipline via the multiset ledger: every
307        // `ManuallyDrop::new` / segment-frame mint adds one entry, every
308        // `Drop::drop` / `ManuallyDrop::new` / segment-frame redeem removes one.
309        &&& self.frame_obligations.len() == 0
310    }
311
312    // ----------------------------------------------------------------------
313    // Frame-side per-instance ledger.
314    // ----------------------------------------------------------------------
315    /// Pairs the production of a per-Frame [`DropObligation`] with a
316    /// `+1` on the `frame_obligations[slot_idx]` count. Called by Frame's
317    /// `constructor_spec` (i.e. `ManuallyDrop::new(frame, ..)`).
318    pub axiom fn tracked_mint_frame_obligation(tracked &mut self, slot_idx: usize) -> (tracked obl:
319        DropObligation<usize>)
320        ensures
321            obl.value() == slot_idx,
322            final(self).frame_obligations =~= old(self).frame_obligations.insert(slot_idx),
323            final(self).slots =~= old(self).slots,
324            final(self).slot_owners =~= old(self).slot_owners,
325    ;
326
327    /// Redeems a per-Frame obligation, decrementing `frame_obligations`
328    /// at `obl.value()`. Called by Frame's `consume_obligation` (i.e.
329    /// by `Drop::drop` or `ManuallyDrop::new`).
330    pub axiom fn tracked_redeem_frame_obligation(
331        tracked &mut self,
332        tracked obl: DropObligation<usize>,
333    )
334        requires
335            old(self).frame_obligations.count(obl.value()) > 0,
336        ensures
337            final(self).frame_obligations =~= old(self).frame_obligations.remove(obl.value()),
338            final(self).slots =~= old(self).slots,
339            final(self).slot_owners =~= old(self).slot_owners,
340    ;
341}
342
343} // verus!
ostd/specs/mm/frame/meta_region_owners.rs

ostd/specs/mm/frame/
meta_region_owners.rs
