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    // The zero variant is reserved for the unused type. Only an unused page
37    // can be designated for one of the other purposes.
38    Unused,
39    /// The page is reserved or unusable. The kernel should not touch it.
40    Reserved,
41    /// The page is used as a frame, i.e., a page of untyped memory.
42    Frame,
43    /// The page is used by a page table.
44    PageTable,
45    /// The page stores metadata of other pages.
46    Meta,
47    /// The page stores the kernel such as kernel code, data, etc.
48    Kernel,
49    /// The page maps memory-mapped I/O (MMIO). Untracked: no refcount, slot
50    /// stays in the free pool, but distinguishable from `Unused` so the
51    /// kernel allocator never collides with an MMIO mapping.
52    MMIO,
53}
54
55/// Whether `pa` falls in an MMIO physical-address range. Uninterpreted at the
56/// spec level — concrete arch- and machine-specific MMIO range layouts are
57/// outside the verification surface, but the kernel allocator (which picks
58/// slots with `PageUsage::Unused`) is guaranteed disjoint from MMIO mappings.
59pub uninterp spec fn is_mmio_paddr(pa: Paddr) -> bool;
60
61/// Connects a slot's `PageUsage::MMIO` discriminant to its paddr's range
62/// membership. Used to derive disjointness between MMIO mappings and the
63/// regular allocator pool: a slot can be `MMIO` iff its paddr is in MMIO
64/// range, so a slot with `usage != MMIO` (e.g. `Unused`) cannot share an idx
65/// with any MMIO mapping.
66pub broadcast axiom fn axiom_mmio_usage_iff_mmio_paddr(slot: MetaSlotOwner)
67    ensures
68        (#[trigger] slot.usage == PageUsage::MMIO) <==> is_mmio_paddr(
69            meta_to_frame(slot.slot_vaddr),
70        ),
71;
72
73/// MMIO ranges are aligned to (and closed under) huge-page granularities:
74/// every sub-paddr within a huge frame inherits the huge frame's MMIO-ness.
75/// This is a hardware-layout convention — MMIO BARs are mapped at huge-page
76/// boundaries, and the verified `split_if_mapped_huge` relies on it to
77/// transfer MMIO-ness from a huge frame to its 4KB sub-pages. Non-broadcast:
78/// callers invoke this explicitly with the relevant `page_size`.
79pub axiom fn axiom_mmio_paddr_huge_page_closed(pa: Paddr, page_size: usize, offset: usize)
80    requires
81        pa % page_size == 0,
82        offset < page_size,
83    ensures
84        is_mmio_paddr((pa + offset) as Paddr) == is_mmio_paddr(pa),
85;
86
87pub struct StoredPageTablePageMeta {
88    pub nr_children: pcell_maybe_uninit::PCell<u16>,
89    pub stray: pcell_maybe_uninit::PCell<bool>,
90    pub level: PagingLevel,
91    pub lock: PAtomicU8,
92}
93
94pub enum MetaSlotStorage {
95    Empty([u8; 39]),
96    Untyped,
97    FrameLink(StoredLink),
98    PTNode(StoredPageTablePageMeta),
99}
100
101/// `MetaSlotStorage` is an inductive tagged union of all of the frame meta types that
102/// we work with in this development. So, it should itself implement `AnyFrameMeta`, and
103/// it can then be used to stand in for `dyn AnyFrameMeta`.
104unsafe impl AnyFrameMeta for MetaSlotStorage {
105    uninterp spec fn vtable_ptr(&self) -> usize;
106}
107
108impl Repr<MetaSlotStorage> for MetaSlotStorage {
109    type ReprPerm = ();
110
111    open spec fn wf(slot: MetaSlotStorage, perm: ()) -> bool {
112        true
113    }
114
115    open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ()) {
116        (self, ())
117    }
118
119    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
120        self
121    }
122
123    open spec fn from_repr_spec(slot: MetaSlotStorage, perm: ()) -> Self {
124        slot
125    }
126
127    fn from_repr(slot: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
128        slot
129    }
130
131    fn from_borrowed<'a>(slot: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
132        slot
133    }
134
135    fn from_borrowed_mut<'a>(
136        slot: &'a mut MetaSlotStorage,
137        Tracked(perm): Tracked<&'a mut ()>,
138    ) -> &'a mut Self {
139        slot
140    }
141
142    proof fn from_to_repr(self, perm: ()) {
143    }
144
145    proof fn to_from_repr(slot: MetaSlotStorage, perm: ()) {
146    }
147
148    proof fn to_repr_wf(self, perm: ()) {
149    }
150}
151
152/// Permissions to access metadata.
153pub tracked struct MetadataPerm {
154    pub storage_perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
155    pub vtable_ptr_perm: vstd::simple_pptr::PointsTo<usize>,
156}
157
158pub const REF_COUNT_MAX_USIZE: usize = REF_COUNT_MAX as usize;
159
160/// Fractional metadata permission.
161pub type FracMetadataPerm = Count<MetadataPerm, REF_COUNT_MAX_USIZE>;
162
163/// The undistributed part of a metadata permission.
164pub type FracMetadataPermResource = CountResource<MetadataPerm, REF_COUNT_MAX_USIZE>;
165
166/// Permissions that remain under the authority of `MetaRegionOwners`.
167///
168/// `ref_count_perm` and `in_list_perm` exist for the complete lifetime of the
169/// corresponding `MetaSlot` (i.e., `'static`).
170pub tracked struct MetaSlotOwner {
171    pub metadata_perm: FracMetadataPermResource,
172    pub ref_count_perm: PermissionU64,
173    pub in_list_perm: PermissionU64,
174    pub ghost slot_vaddr: Vaddr,
175    pub ghost usage: PageUsage,
176    /// The set of tree paths at which this slot is referenced. For PT-node
177    /// slots this is a singleton. For data-frame slots this tracks every
178    /// location the frame is currently mapped — allowing a single frame to be
179    /// mapped at multiple addresses.
180    pub ghost paths_in_pt: Set<TreePath<NR_ENTRIES>>,
181}
182
183impl MetaSlotOwner {
184    pub open spec fn same_permissions(self, other: Self) -> bool {
185        &&& self.metadata_perm == other.metadata_perm
186        &&& self.ref_count_perm == other.ref_count_perm
187        &&& self.in_list_perm == other.in_list_perm
188    }
189
190    pub open spec fn ref_count(self) -> u64 {
191        self.ref_count_perm.value()
192    }
193
194    pub open spec fn metadata_perm(self) -> MetadataPerm {
195        self.metadata_perm.resource()
196    }
197
198    pub open spec fn storage_perm(self) -> pcell_maybe_uninit::PointsTo<MetaSlotStorage> {
199        self.metadata_perm().storage_perm
200    }
201
202    pub open spec fn vtable_ptr_perm(self) -> vstd::simple_pptr::PointsTo<usize> {
203        self.metadata_perm().vtable_ptr_perm
204    }
205
206    pub proof fn tracked_borrow_metadata_perm(tracked &self) -> tracked &MetadataPerm
207        requires
208            !self.metadata_perm.is_resource_vacant(),
209        returns
210            self.metadata_perm(),
211    {
212        self.metadata_perm.tracked_borrow()
213    }
214}
215
216/// Well-formedness of a concrete metadata representation.
217pub open spec fn typed_meta_wf<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
218    slot_perm: vstd::simple_pptr::PointsTo<MetaSlot>,
219    metadata_perm: MetadataPerm,
220    repr_perm: M::ReprPerm,
221) -> bool {
222    &&& slot_perm.is_init()
223    &&& MetaSlot::perms_related(slot_perm, metadata_perm)
224    &&& M::wf(metadata_perm.storage_perm.value(), repr_perm)
225}
226
227/// The value of a concrete metadata.
228pub open spec fn typed_meta_value<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
229    metadata_perm: MetadataPerm,
230    repr_perm: M::ReprPerm,
231) -> M {
232    M::from_repr_spec(metadata_perm.storage_perm.value(), repr_perm)
233}
234
235pub fn borrow_meta<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
236    ptr: cast_ptr::ReprPtr<MetaSlotStorage, M>,
237    Tracked(slot_perm): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
238    Tracked(metadata_perm): Tracked<&'a MetadataPerm>,
239    Tracked(repr_perm): Tracked<&'a M::ReprPerm>,
240) -> &'a M
241    requires
242        ptr.addr() == slot_perm.addr(),
243        typed_meta_wf::<M>(*slot_perm, *metadata_perm, *repr_perm),
244    returns
245        typed_meta_value::<M>(*metadata_perm, *repr_perm),
246{
247    let slot = PPtr::<MetaSlot>::from_addr(ptr.addr()).borrow(Tracked(slot_perm));
248    M::from_borrowed(slot.storage.borrow(Tracked(&metadata_perm.storage_perm)), Tracked(repr_perm))
249}
250
251pub fn borrow_meta_mut<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
252    ptr: cast_ptr::ReprPtr<MetaSlotStorage, M>,
253    Tracked(slot_perm): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
254    Tracked(metadata_perms): Tracked<&'a mut MetadataPerm>,
255    Tracked(repr_perm): Tracked<&'a mut M::ReprPerm>,
256) -> (res: &'a mut M)
257    requires
258        ptr.addr() == slot_perm.addr(),
259        typed_meta_wf::<M>(*slot_perm, *old(metadata_perms), *old(repr_perm)),
260    ensures
261        *res == typed_meta_value::<M>(*old(metadata_perms), *old(repr_perm)),
262        *final(res) == typed_meta_value::<M>(*final(metadata_perms), *final(repr_perm)),
263        typed_meta_wf::<M>(*slot_perm, *final(metadata_perms), *final(repr_perm)),
264{
265    let slot = PPtr::<MetaSlot>::from_addr(ptr.addr()).borrow(Tracked(slot_perm));
266    M::from_borrowed_mut(
267        slot.storage.borrow_mut(Tracked(&mut metadata_perms.storage_perm)),
268        Tracked(repr_perm),
269    )
270}
271
272impl Inv for MetaSlotOwner {
273    open spec fn inv(self) -> bool {
274        &&& self.ref_count() == REF_COUNT_UNUSED ==> {
275            &&& self.metadata_perm.is_full()
276            &&& self.storage_perm().is_uninit()
277            &&& self.vtable_ptr_perm().is_uninit()
278            &&& self.in_list_perm.value()
279                == 0
280            // A managed slot at `REF_COUNT_UNUSED` has no live PTE mapping.
281            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
282        }
283        &&& self.ref_count() == REF_COUNT_UNIQUE ==> {
284            &&& self.metadata_perm.is_resource_vacant()
285            &&& (self.usage != PageUsage::MMIO ==> self.paths_in_pt.is_empty())
286        }
287        &&& 0 < self.ref_count() <= REF_COUNT_MAX ==> {
288            &&& self.metadata_perm.frac() + self.ref_count() == REF_COUNT_MAX
289            &&& self.vtable_ptr_perm().is_init()
290            &&& self.storage_perm().is_init()
291            &&& self.in_list_perm.value() == 0
292        }
293        &&& REF_COUNT_MAX < self.ref_count() < REF_COUNT_UNIQUE ==> { false }
294        &&& self.ref_count() == 0 ==> {
295            &&& self.in_list_perm.value() == 0
296        }
297        &&& FRAME_METADATA_RANGE.start <= self.slot_vaddr < FRAME_METADATA_RANGE.end
298        &&& self.slot_vaddr % META_SLOT_SIZE == 0
299    }
300}
301
302impl OwnerOf for MetaSlot {
303    type Owner = MetaSlotOwner;
304
305    open spec fn wf(self, owner: Self::Owner) -> bool {
306        &&& self.ref_count.id() == owner.ref_count_perm.id()
307        &&& self.in_list.id() == owner.in_list_perm.id()
308        &&& owner.metadata_perm.not_empty() ==> {
309            &&& self.storage.id() == owner.storage_perm().id()
310            &&& self.vtable_ptr == owner.vtable_ptr_perm().pptr()
311        }
312    }
313}
314
315/// Writes `metadata` into the byte storage and establishes its direct
316/// `Repr<MetaSlotStorage>` interpretation.
317pub exec fn write_metadata_into_storage<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
318    cell: &pcell_maybe_uninit::PCell<MetaSlotStorage>,
319    Tracked(metadata_perms): Tracked<&mut MetadataPerm>,
320    Tracked(repr_perm): Tracked<&mut M::ReprPerm>,
321    metadata: M,
322)
323    requires
324        cell.id() == old(metadata_perms).storage_perm.id(),
325    ensures
326        final(metadata_perms).storage_perm.id() == old(metadata_perms).storage_perm.id(),
327        final(metadata_perms).storage_perm.is_init(),
328        final(metadata_perms).vtable_ptr_perm == old(metadata_perms).vtable_ptr_perm,
329        M::wf(final(metadata_perms).storage_perm.value(), *final(repr_perm)),
330        M::from_repr_spec(final(metadata_perms).storage_perm.value(), *final(repr_perm))
331            == metadata,
332{
333    proof {
334        M::from_to_repr(metadata, *repr_perm);
335        M::to_repr_wf(metadata, *repr_perm);
336    }
337    let repr = metadata.to_repr(Tracked(repr_perm));
338    cell.write(Tracked(&mut metadata_perms.storage_perm), repr);
339}
340
341} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
