ostd/specs/mm/mod.rs
1pub mod cpu;
2pub mod frame;
3pub mod io;
4pub mod page_table;
5pub mod pod;
6pub mod tlb;
7pub mod virt_mem_newer;
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, Mapping, PageTableOwner, PageTableView, INC_LEVELS};
17use crate::specs::mm::tlb::TlbModel;
18use crate::specs::mm::virt_mem_newer::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
49 /// The set of mappings in the page table is determined by
50 /// [`PageTableOwner::view_rec`](crate::specs::mm::page_table::owners::PageTableOwner::view_rec).
51 pub closed spec fn page_table_mappings(self) -> Set<Mapping> {
52 self.pt.view_rec(self.pt.0.value.path)
53 }
54
55 /// Top-level property: the page table mappings are disjoint in the virtual address space.
56 pub open spec fn page_table_mappings_disjoint_vaddrs(self) -> bool {
57 let pt_mappings = self.page_table_mappings();
58 forall |m1: Mapping, m2: Mapping|
59 pt_mappings has m1 &&
60 pt_mappings has m2 &&
61 m1 != m2 ==>
62 Mapping::disjoint_vaddrs(m1, m2)
63 }
64
65 /// Top-level property: the page table mappings are well-formed.
66 /// See [`Mapping::inv`](crate::specs::mm::page_table::view::Mapping::inv).
67 pub open spec fn page_table_mappings_well_formed(self) -> bool {
68 let pt_mappings = self.page_table_mappings();
69 forall |m: Mapping|
70 pt_mappings has m ==>
71 #[trigger] m.inv()
72 }
73
74 /// Top-level property: the TLB mappings are disjoint in the virtual address space.
75 pub open spec fn tlb_mappings_disjoint_vaddrs(self) -> bool {
76 let tlb_mappings = self.tlb.mappings;
77 forall |m1: Mapping, m2: Mapping|
78 tlb_mappings has m1 &&
79 tlb_mappings has m2 &&
80 m1 != m2 ==>
81 Mapping::disjoint_vaddrs(m1, m2)
82 }
83
84 /// Top-level property: the TLB mappings are disjoint in the physical address space.
85 pub open spec fn tlb_mappings_disjoint_paddrs(self) -> bool {
86 let tlb_mappings = self.tlb.mappings;
87 forall |m1: Mapping, m2: Mapping|
88 tlb_mappings has m1 &&
89 tlb_mappings has m2 &&
90 m1 != m2 ==>
91 Mapping::disjoint_paddrs(m1, m2)
92 }
93
94 /// Top-level property: the TLB mappings are well-formed.
95 pub open spec fn tlb_mappings_well_formed(self) -> bool {
96 let tlb_mappings = self.tlb.mappings;
97 forall |m: Mapping|
98 tlb_mappings has m ==>
99 #[trigger] m.inv()
100 }
101
102 /// Top-level properties: the page table mappings are disjoint in the
103 /// virtual address space and well-formed. Disjointness in the *physical*
104 /// address space is intentionally **not** claimed — shared frame mappings
105 /// (Phase 3 of the `paths_in_pt` refactor) legitimately map the same
106 /// paddr at multiple vaddrs.
107 pub open spec fn invariants(self) -> bool {
108 &&& self.page_table_mappings_disjoint_vaddrs()
109 &&& self.page_table_mappings_well_formed()
110 }
111
112 /// Internal invariants for [`GlobalMemOwner`]: the page table is consistent with the TLB
113 /// and with the allocated regions, and the internal invariants of each component hold.
114 /// Note that some API functions break the consistency between the page table and the TLB,
115 /// making it the responsibility of the caller to restore it by flushing the TLB.
116 pub open spec fn internal_invariants(self) -> bool {
117 &&& self.regions.inv()
118 &&& self.pt.inv()
119 &&& self.pt.metaregion_sound(self.regions)
120 &&& self.tlb.consistent_with_pt(self.pt.view())
121 }
122
123 /// If the internal invariants hold, then the top-level properties hold.
124 pub proof fn internal_invariants_imply_top_level_properties(self)
125 requires
126 self.internal_invariants(),
127 ensures
128 self.invariants(),
129 {
130 let pt = self.pt;
131 let root_path = pt.0.value.path;
132
133 assert forall |m1: Mapping, m2: Mapping|
134 self.page_table_mappings() has m1
135 && self.page_table_mappings() has m2
136 && m1 != m2
137 implies #[trigger] Mapping::disjoint_vaddrs(m1, m2) by {
138 pt.view_rec_disjoint_vaddrs(root_path, m1, m2);
139 }
140
141 pt.view_rec_mapping_inv(root_path);
142 }
143}
144
145} // verus!