ostd/specs/mm/mod.rs
1pub mod cpu;
2pub mod frame;
3pub mod page_table;
4pub mod tlb;
5pub mod virt_mem_newer;
6
7use vstd::prelude::*;
8
9use vstd_extra::ownership::*;
10
11use crate::mm::vm_space::UserPtConfig;
12use crate::mm::{Paddr, Vaddr};
13use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
14use crate::specs::mm::page_table::{Guards, Mapping, PageTableOwner, PageTableView};
15use crate::specs::mm::tlb::TlbModel;
16use crate::specs::mm::virt_mem_newer::FrameContents;
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
47 /// The set of mappings in the page table is determined by
48 /// [`PageTableOwner::view_rec`](crate::specs::mm::page_table::owners::PageTableOwner::view_rec).
49 pub closed spec fn page_table_mappings(self) -> Set<Mapping> {
50 self.pt.view_rec(self.pt.0.value.path)
51 }
52
53 /// Top-level property: the page table mappings are disjoint in the virtual address space.
54 pub open spec fn page_table_mappings_disjoint_vaddrs(self) -> bool {
55 let pt_mappings = self.page_table_mappings();
56 forall |m1: Mapping, m2: Mapping|
57 pt_mappings has m1 &&
58 pt_mappings has m2 &&
59 m1 != m2 ==>
60 Mapping::disjoint_vaddrs(m1, m2)
61 }
62
63 /// Top-level property: the page table mappings are disjoint in the physical address space.
64 pub open spec fn page_table_mappings_disjoint_paddrs(self) -> bool {
65 let pt_mappings = self.page_table_mappings();
66 forall |m1: Mapping, m2: Mapping|
67 pt_mappings has m1 &&
68 pt_mappings has m2 &&
69 m1 != m2 ==>
70 Mapping::disjoint_paddrs(m1, m2)
71 }
72
73 /// Top-level property: the page table mappings are well-formed.
74 /// See [`Mapping::inv`](crate::specs::mm::page_table::view::Mapping::inv).
75 pub open spec fn page_table_mappings_well_formed(self) -> bool {
76 let pt_mappings = self.page_table_mappings();
77 forall |m: Mapping|
78 pt_mappings has m ==>
79 #[trigger] m.inv()
80 }
81
82 /// Top-level property: the TLB mappings are disjoint in the virtual address space.
83 pub open spec fn tlb_mappings_disjoint_vaddrs(self) -> bool {
84 let tlb_mappings = self.tlb.mappings;
85 forall |m1: Mapping, m2: Mapping|
86 tlb_mappings has m1 &&
87 tlb_mappings has m2 &&
88 m1 != m2 ==>
89 Mapping::disjoint_vaddrs(m1, m2)
90 }
91
92 /// Top-level property: the TLB mappings are disjoint in the physical address space.
93 pub open spec fn tlb_mappings_disjoint_paddrs(self) -> bool {
94 let tlb_mappings = self.tlb.mappings;
95 forall |m1: Mapping, m2: Mapping|
96 tlb_mappings has m1 &&
97 tlb_mappings has m2 &&
98 m1 != m2 ==>
99 Mapping::disjoint_paddrs(m1, m2)
100 }
101
102 /// Top-level property: the TLB mappings are well-formed.
103 pub open spec fn tlb_mappings_well_formed(self) -> bool {
104 let tlb_mappings = self.tlb.mappings;
105 forall |m: Mapping|
106 tlb_mappings has m ==>
107 #[trigger] m.inv()
108 }
109
110 /// Top-level properties: the page table mappings are disjoint and well-formed.
111 pub open spec fn invariants(self) -> bool {
112 &&& self.page_table_mappings_disjoint_vaddrs()
113 &&& self.page_table_mappings_disjoint_paddrs()
114 &&& self.page_table_mappings_well_formed()
115 }
116
117 /// Internal invariants for [`GlobalMemOwner`]: the page table is consistent with the TLB
118 /// and with the allocated regions, and the internal invariants of each component hold.
119 /// Note that some API functions break the consistency between the page table and the TLB,
120 /// making it the responsibility of the caller to restore it by flushing the TLB.
121 pub open spec fn internal_invariants(self) -> bool {
122 &&& self.regions.inv()
123 &&& self.pt.inv()
124 &&& self.pt.relate_region(self.regions)
125 &&& self.tlb.consistent_with_pt(self.pt.view())
126 }
127
128 /// If the internal invariants hold, then the top-level properties hold.
129 /// The key lemmas here are
130 /// [`view_rec_disjoint_vaddrs`](crate::specs::mm::page_table::owners::PageTableOwner::view_rec_disjoint_vaddrs)
131 /// and [`view_rec_disjoint_paddrs`](crate::specs::mm::page_table::owners::PageTableOwner::view_rec_disjoint_paddrs).
132 pub proof fn internal_invariants_imply_top_level_properties(self)
133 requires
134 self.internal_invariants(),
135 ensures
136 self.invariants(),
137 {
138 assert(self.invariants()) by {
139 // This follows from `view_rec_disjoint_vaddrs` and `view_rec_disjoint_paddrs`.
140 // Just need to wire them together properly.
141 admit();
142 };
143 }
144}
145
146} // verus!