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