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

ostd/specs/mm/frame/
meta_region_owners.rs
