ostd/specs/mm/frame/
meta_owners.rs

1use vstd::{atomic::*, cell::pcell_maybe_uninit, prelude::*, simple_pptr::*};
2use vstd_extra::{
3    cast_ptr::{self, Repr},
4    ghost_tree::TreePath,
5    ownership::*,
6    resource::ghost_resource::count_auth::{Count, CountResource},
7};
8
9use crate::specs::{arch::NR_ENTRIES, mm::frame::linked_list::linked_list_owners::StoredLink};
10
11use super::*;
12use crate::mm::{
13    Paddr, PagingLevel, Vaddr,
14    frame::{
15        AnyFrameMeta,
16        meta::{
17            META_SLOT_SIZE, MetaSlot, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
18            mapping::meta_to_frame,
19        },
20    },
21    kspace::FRAME_METADATA_RANGE,
22};
23
24verus! {
25
26#[allow(non_camel_case_types)]
27pub ghost enum MetaSlotStatus {
28    UNUSED,
29    UNIQUE,
30    SHARED,
31    OVERFLOW,
32    UNDER_CONSTRUCTION,
33}
34
35pub ghost enum PageUsage {
36    /// Initial purpose before metadata is installed. Reuse is governed by refcount.
37    Unused,
38    /// The page is reserved or unusable. The kernel should not touch it.
39    Reserved,
40    /// The page is used as a frame, i.e., a page of untyped memory.
41    Frame,
42    /// The page is used by a page table.
43    PageTable,
44    /// The page stores metadata of other pages.
45    Meta,
46    /// The page stores the kernel such as kernel code, data, etc.
47    Kernel,
48}
49
50pub struct StoredPageTablePageMeta {
51    pub nr_children: pcell_maybe_uninit::PCell<u16>,
52    pub stray: pcell_maybe_uninit::PCell<bool>,
53    pub level: PagingLevel,
54    pub lock: PAtomicU8,
55}
56
57pub enum MetaSlotStorage {
58    Empty([u8; 39]),
59    Untyped,
60    FrameLink(StoredLink),
61    PTNode(StoredPageTablePageMeta),
62}
63
64impl MetaSlotStorage {
65    /// The purpose established by the installed metadata representation.
66    pub open spec fn usage(self) -> PageUsage {
67        if self is PTNode {
68            PageUsage::PageTable
69        } else {
70            PageUsage::Frame
71        }
72    }
73}
74
75/// `MetaSlotStorage` is an inductive tagged union of all of the frame meta types that
76/// we work with in this development. So, it should itself implement `AnyFrameMeta`, and
77/// it can then be used to stand in for `dyn AnyFrameMeta`.
78unsafe impl AnyFrameMeta for MetaSlotStorage {
79    uninterp spec fn vtable_ptr(&self) -> usize;
80}
81
82impl Repr<MetaSlotStorage> for MetaSlotStorage {
83    type ReprPerm = ();
84
85    open spec fn wf(slot: MetaSlotStorage, perm: ()) -> bool {
86        true
87    }
88
89    open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ()) {
90        (self, ())
91    }
92
93    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
94        self
95    }
96
97    open spec fn from_repr_spec(slot: MetaSlotStorage, perm: ()) -> Self {
98        slot
99    }
100
101    fn from_repr(slot: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
102        slot
103    }
104
105    fn from_borrowed<'a>(slot: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
106        slot
107    }
108
109    fn from_borrowed_mut<'a>(
110        slot: &'a mut MetaSlotStorage,
111        Tracked(perm): Tracked<&'a mut ()>,
112    ) -> &'a mut Self {
113        slot
114    }
115
116    proof fn from_to_repr(self, perm: ()) {
117    }
118
119    proof fn to_from_repr(slot: MetaSlotStorage, perm: ()) {
120    }
121
122    proof fn to_repr_wf(self, perm: ()) {
123    }
124}
125
126/// Permissions to access metadata.
127pub tracked struct MetadataPerm {
128    pub storage_perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
129    pub vtable_ptr_perm: vstd::simple_pptr::PointsTo<usize>,
130}
131
132impl MetadataPerm {
133    /// The purpose of the metadata described by this permission.
134    pub open spec fn usage(self) -> PageUsage {
135        self.storage_perm.value().usage()
136    }
137}
138
139pub const REF_COUNT_MAX_USIZE: usize = REF_COUNT_MAX as usize;
140
141/// Fractional metadata permission.
142pub type FracMetadataPerm = Count<MetadataPerm, REF_COUNT_MAX_USIZE>;
143
144/// The undistributed part of a metadata permission.
145pub type FracMetadataPermResource = CountResource<MetadataPerm, REF_COUNT_MAX_USIZE>;
146
147/// Permissions that remain under the authority of `MetaRegionOwners`.
148///
149/// `ref_count_perm` and `in_list_perm` exist for the complete lifetime of the
150/// corresponding `MetaSlot` (i.e., `'static`).
151pub tracked struct MetaSlotOwner {
152    pub metadata_perm: FracMetadataPermResource,
153    pub ref_count_perm: PermissionU64,
154    pub in_list_perm: PermissionU64,
155    pub ghost slot_vaddr: Vaddr,
156    pub ghost usage: PageUsage,
157    /// The set of tree paths at which this slot is referenced. For PT-node
158    /// slots this is a singleton. For data-frame slots this tracks every
159    /// location the frame is currently mapped — allowing a single frame to be
160    /// mapped at multiple addresses.
161    pub ghost paths_in_pt: Set<TreePath<NR_ENTRIES>>,
162}
163
164impl MetaSlotOwner {
165    pub open spec fn same_permissions(self, other: Self) -> bool {
166        &&& self.metadata_perm == other.metadata_perm
167        &&& self.ref_count_perm == other.ref_count_perm
168        &&& self.in_list_perm == other.in_list_perm
169    }
170
171    pub open spec fn ref_count(self) -> u64 {
172        self.ref_count_perm.value()
173    }
174
175    pub open spec fn metadata_perm(self) -> MetadataPerm {
176        self.metadata_perm.resource()
177    }
178
179    pub open spec fn storage_perm(self) -> pcell_maybe_uninit::PointsTo<MetaSlotStorage> {
180        self.metadata_perm().storage_perm
181    }
182
183    pub open spec fn vtable_ptr_perm(self) -> vstd::simple_pptr::PointsTo<usize> {
184        self.metadata_perm().vtable_ptr_perm
185    }
186
187    pub proof fn tracked_borrow_metadata_perm(tracked &self) -> tracked &MetadataPerm
188        requires
189            !self.metadata_perm.is_resource_vacant(),
190        returns
191            self.metadata_perm(),
192    {
193        self.metadata_perm.tracked_borrow()
194    }
195}
196
197/// Well-formedness of a concrete metadata representation.
198pub open spec fn typed_meta_wf<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
199    slot_perm: vstd::simple_pptr::PointsTo<MetaSlot>,
200    metadata_perm: MetadataPerm,
201    repr_perm: M::ReprPerm,
202) -> bool {
203    &&& slot_perm.is_init()
204    &&& MetaSlot::perms_related(slot_perm, metadata_perm)
205    &&& M::wf(metadata_perm.storage_perm.value(), repr_perm)
206}
207
208/// The value of a concrete metadata.
209pub open spec fn typed_meta_value<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
210    metadata_perm: MetadataPerm,
211    repr_perm: M::ReprPerm,
212) -> M {
213    M::from_repr_spec(metadata_perm.storage_perm.value(), repr_perm)
214}
215
216pub fn borrow_meta<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
217    ptr: cast_ptr::ReprPtr<MetaSlotStorage, M>,
218    Tracked(slot_perm): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
219    Tracked(metadata_perm): Tracked<&'a MetadataPerm>,
220    Tracked(repr_perm): Tracked<&'a M::ReprPerm>,
221) -> &'a M
222    requires
223        ptr.addr() == slot_perm.addr(),
224        typed_meta_wf::<M>(*slot_perm, *metadata_perm, *repr_perm),
225    returns
226        typed_meta_value::<M>(*metadata_perm, *repr_perm),
227{
228    let slot = PPtr::<MetaSlot>::from_addr(ptr.addr()).borrow(Tracked(slot_perm));
229    M::from_borrowed(slot.storage.borrow(Tracked(&metadata_perm.storage_perm)), Tracked(repr_perm))
230}
231
232pub fn borrow_meta_mut<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
233    ptr: cast_ptr::ReprPtr<MetaSlotStorage, M>,
234    Tracked(slot_perm): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
235    Tracked(metadata_perms): Tracked<&'a mut MetadataPerm>,
236    Tracked(repr_perm): Tracked<&'a mut M::ReprPerm>,
237) -> (res: &'a mut M)
238    requires
239        ptr.addr() == slot_perm.addr(),
240        typed_meta_wf::<M>(*slot_perm, *old(metadata_perms), *old(repr_perm)),
241    ensures
242        *res == typed_meta_value::<M>(*old(metadata_perms), *old(repr_perm)),
243        *final(res) == typed_meta_value::<M>(*final(metadata_perms), *final(repr_perm)),
244        typed_meta_wf::<M>(*slot_perm, *final(metadata_perms), *final(repr_perm)),
245{
246    let slot = PPtr::<MetaSlot>::from_addr(ptr.addr()).borrow(Tracked(slot_perm));
247    M::from_borrowed_mut(
248        slot.storage.borrow_mut(Tracked(&mut metadata_perms.storage_perm)),
249        Tracked(repr_perm),
250    )
251}
252
253impl Inv for MetaSlotOwner {
254    open spec fn inv(self) -> bool {
255        &&& self.ref_count() == REF_COUNT_UNUSED ==> {
256            &&& self.metadata_perm.is_full()
257            &&& self.storage_perm().is_uninit()
258            &&& self.vtable_ptr_perm().is_uninit()
259            &&& self.in_list_perm.value() == 0
260            &&& self.paths_in_pt.is_empty()
261        }
262        &&& self.ref_count() == REF_COUNT_UNIQUE ==> {
263            &&& self.metadata_perm.is_resource_vacant()
264            &&& self.paths_in_pt.is_empty()
265        }
266        &&& 0 < self.ref_count() <= REF_COUNT_MAX ==> {
267            &&& self.metadata_perm.frac() + self.ref_count() == REF_COUNT_MAX
268            &&& self.vtable_ptr_perm().is_init()
269            &&& self.storage_perm().is_init()
270            &&& self.in_list_perm.value() == 0
271        }
272        &&& REF_COUNT_MAX < self.ref_count() < REF_COUNT_UNIQUE ==> { false }
273        &&& self.ref_count() == 0 ==> {
274            &&& self.metadata_perm.is_full()
275            &&& self.in_list_perm.value() == 0
276        }
277        &&& FRAME_METADATA_RANGE.start <= self.slot_vaddr < FRAME_METADATA_RANGE.end
278        &&& self.slot_vaddr % META_SLOT_SIZE == 0
279    }
280}
281
282impl OwnerOf for MetaSlot {
283    type Owner = MetaSlotOwner;
284
285    open spec fn wf(self, owner: Self::Owner) -> bool {
286        &&& self.ref_count.id() == owner.ref_count_perm.id()
287        &&& self.in_list.id() == owner.in_list_perm.id()
288        &&& owner.metadata_perm.not_empty() ==> {
289            &&& self.storage.id() == owner.storage_perm().id()
290            &&& self.vtable_ptr == owner.vtable_ptr_perm().pptr()
291        }
292    }
293}
294
295/// Writes `metadata` into the byte storage and establishes its direct
296/// `Repr<MetaSlotStorage>` interpretation.
297pub exec fn write_metadata_into_storage<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
298    cell: &pcell_maybe_uninit::PCell<MetaSlotStorage>,
299    Tracked(metadata_perms): Tracked<&mut MetadataPerm>,
300    Tracked(repr_perm): Tracked<&mut M::ReprPerm>,
301    metadata: M,
302)
303    requires
304        cell.id() == old(metadata_perms).storage_perm.id(),
305    ensures
306        final(metadata_perms).storage_perm.id() == old(metadata_perms).storage_perm.id(),
307        final(metadata_perms).storage_perm.is_init(),
308        final(metadata_perms).vtable_ptr_perm == old(metadata_perms).vtable_ptr_perm,
309        M::wf(final(metadata_perms).storage_perm.value(), *final(repr_perm)),
310        M::from_repr_spec(final(metadata_perms).storage_perm.value(), *final(repr_perm))
311            == metadata,
312{
313    proof {
314        M::from_to_repr(metadata, *repr_perm);
315        M::to_repr_wf(metadata, *repr_perm);
316    }
317    let repr = metadata.to_repr(Tracked(repr_perm));
318    cell.write(Tracked(&mut metadata_perms.storage_perm), repr);
319}
320
321} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
