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