ostd/specs/mm/
mod.rs

1pub mod embedding;
2pub mod frame;
3pub mod io;
4pub mod page_table;
5pub mod tlb;
6pub mod virt_mem;
7
8use vstd::prelude::*;
9use vstd_extra::ownership::*;
10
11use crate::specs::mm::{
12    frame::meta_region_owners::MetaRegionOwners, page_table::*, tlb::TlbModel,
13    virt_mem::FrameContents,
14};
15
16use crate::mm::{Paddr, PagingConstsTrait, Vaddr, vm_space::UserPtConfig};
17
18verus! {
19
20/// # Global memory invariants
21/// A [`GlobalMemOwner`] object ties together the components that are used in different layers
22/// of the OSTD system. It is the object about which we state the invariants of the
23/// memory system as a whole.
24/// ## Verification Structure
25/// Operations in `mm` take pieces of the global state as mutable arguments,
26/// and guarantee that their invariants are preserved. This guarantees that, at the end of each
27/// operation, the overall [`internal_invariants`](GlobalMemOwner::internal_invariants) of the system
28/// hold. We then prove that the internal invariants imply the top-level properties that we want the
29/// memory system to obey.
30pub tracked struct GlobalMemOwner {
31    /// [`MetaRegionOwners`] is the fundamental data structure of the `frame` module, tracking the allocation
32    /// of metadata slots and their permissions.
33    pub regions: MetaRegionOwners,
34    /// [`PageTableOwner`] tracks the tree structure of the page table. It can be converted to a
35    /// [`CursorOwner`] for traversal and updates.
36    /// A well-formed `CursorOwner` can be converted back into a `PageTableOwner` with consistent mappings,
37    /// ensuring that its internal invariants are preserved.
38    pub pt: PageTableOwner<UserPtConfig>,
39    /// [`TlbModel`] tracks the mappings in the TLB. It can flush mappings and it can load new ones from the page table.
40    pub tlb: TlbModel,
41    /// [`FrameContents`] tracks the contents of a frame for use in the [`VirtMem`] library.
42    pub memory: Map<Paddr, FrameContents>,
43}
44
45impl GlobalMemOwner {
46    /// The set of mappings in the page table is determined by
47    /// [`PageTableOwner::view_rec`](crate::specs::mm::page_table::owners::PageTableOwner::view_rec).
48    pub closed spec fn page_table_mappings(self) -> Set<Mapping> {
49        self.pt.view_rec(self.pt.0.value().path)
50    }
51
52    /// Top-level property: the page table mappings are disjoint in the virtual address space.
53    pub open spec fn page_table_mappings_disjoint_vaddrs(self) -> bool {
54        mappings_disjoint_vaddrs(self.page_table_mappings())
55    }
56
57    /// Top-level property: the page table mappings are well-formed.
58    /// See [`Mapping::inv`](crate::specs::mm::page_table::view::Mapping::inv).
59    pub open spec fn page_table_mappings_well_formed(self) -> bool {
60        mappings_well_formed(self.page_table_mappings())
61    }
62
63    /// Top-level property: the TLB mappings are disjoint in the virtual address space.
64    pub open spec fn tlb_mappings_disjoint_vaddrs(self) -> bool {
65        mappings_disjoint_vaddrs(self.tlb.mappings)
66    }
67
68    /// Top-level property: the TLB mappings are disjoint in the physical address space.
69    pub open spec fn tlb_mappings_disjoint_paddrs(self) -> bool {
70        mappings_disjoint_paddrs(self.tlb.mappings)
71    }
72
73    /// Top-level property: the TLB mappings are well-formed.
74    pub open spec fn tlb_mappings_well_formed(self) -> bool {
75        mappings_well_formed(self.tlb.mappings)
76    }
77
78    /// Top-level properties: the page table mappings are disjoint in the
79    /// virtual address space and well-formed. Disjointness in the *physical*
80    /// address space is intentionally **not** claimed — shared frame mappings
81    /// (Phase 3 of the `paths_in_pt` refactor) legitimately map the same
82    /// paddr at multiple vaddrs.
83    pub open spec fn invariants(self) -> bool {
84        &&& self.page_table_mappings_disjoint_vaddrs()
85        &&& self.page_table_mappings_well_formed()
86    }
87
88    /// Internal invariants for [`GlobalMemOwner`]: the page table is consistent with the TLB
89    /// and with the allocated regions, and the internal invariants of each component hold.
90    /// Note that some API functions break the consistency between the page table and the TLB,
91    /// making it the responsibility of the caller to restore it by flushing the TLB.
92    pub open spec fn internal_invariants(self) -> bool {
93        &&& self.regions.inv()
94        &&& self.pt.inv()
95        &&& self.pt.metaregion_sound(self.regions)
96        &&& self.tlb.consistent_with_pt(self.pt.view())
97    }
98
99    /// If the internal invariants hold, then the top-level properties hold.
100    pub proof fn internal_invariants_imply_top_level_properties(self)
101        requires
102            self.internal_invariants(),
103        ensures
104            self.invariants(),
105    {
106        let pt = self.pt;
107        let root_path = pt.0.value().path;
108
109        assert forall|m1: Mapping, m2: Mapping|
110            self.page_table_mappings() has m1 && self.page_table_mappings() has m2 && m1
111                != m2 implies #[trigger] Mapping::disjoint_vaddrs(m1, m2) by {
112            pt.lemma_view_rec_disjoint_vaddrs(root_path, m1, m2);
113        }
114
115        pt.lemma_view_rec_mapping_inv(root_path);
116    }
117}
118
119} // verus!
ostd/specs/mm/mod.rs

ostd/specs/mm/
mod.rs
