ostd/mm/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Virtual memory (VM).
3use crate::specs::arch::*;
4use vstd::arithmetic::div_mod::group_div_basics;
5use vstd::arithmetic::power2::*;
6use vstd::prelude::*;
7
8/// Virtual addresses.
9pub type Vaddr = usize;
10
11/// Physical addresses.
12pub type Paddr = usize;
13
14pub(crate) mod dma;
15pub mod frame;
16//pub mod heap;
17pub mod io;
18pub mod kspace;
19pub(crate) mod page_prop;
20pub mod page_table;
21pub mod tlb;
22pub mod vm_space;
23
24#[cfg(ktest)]
25mod test;
26
27use core::{fmt::Debug, ops::Range};
28
29pub use self::{
30    dma::{Daddr, DmaCoherent, /* DmaDirection, DmaStream, DmaStreamSlice, */ HasDaddr},
31    frame::{
32        Frame,
33        allocator::FrameAllocOptions,
34        segment::{Segment, USegment},
35        unique::UniqueFrame,
36        untyped::{AnyUFrameMeta, UFrame, UntypedMem},
37    },
38    io::{
39        Fallible, FallibleVmRead, FallibleVmWrite, Infallible, PodOnce, VmIo, VmIoOnce, VmReader,
40        VmWriter,
41    },
42    page_prop::{CachePolicy, PageFlags, PageProperty},
43    vm_space::VmSpace,
44};
45pub(crate) use self::{
46    kspace::paddr_to_vaddr, page_prop::PrivilegedPageFlags, page_table::PageTable,
47};
48pub(crate) use crate::arch::mm::PagingConsts;
49
50// Re-export largest_pages from page_table
51pub(crate) use page_table::largest_pages;
52
53/// The level of a page table node or a frame.
54pub type PagingLevel = u8;
55
56verus! {
57
58/// A minimal set of constants that determines the paging system.
59/// This provides an abstraction over most paging modes in common architectures.
60pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static {
61    spec fn BASE_PAGE_SIZE_spec() -> usize;
62
63    /// The smallest page size.
64    /// This is also the page size at level 1 page tables.
65    #[verifier::when_used_as_spec(BASE_PAGE_SIZE_spec)]
66    fn BASE_PAGE_SIZE() -> (res: usize)
67        returns
68            Self::BASE_PAGE_SIZE(),
69    ;
70
71    spec fn NR_LEVELS_spec() -> PagingLevel;
72
73    /// The number of levels in the page table.
74    /// The numbering of levels goes from deepest node to the root node. For example,
75    /// the level 1 to 5 on AMD64 corresponds to Page Tables, Page Directory Tables,
76    /// Page Directory Pointer Tables, Page-Map Level-4 Table, and Page-Map Level-5
77    /// Table, respectively.
78    #[verifier::when_used_as_spec(NR_LEVELS_spec)]
79    fn NR_LEVELS() -> (res: PagingLevel)
80        returns
81            Self::NR_LEVELS(),
82    ;
83
84    spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel;
85
86    /// The highest level that a PTE can be directly used to translate a VA.
87    /// This affects the the largest page size supported by the page table.
88    #[verifier::when_used_as_spec(HIGHEST_TRANSLATION_LEVEL_spec)]
89    fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel
90        returns
91            Self::HIGHEST_TRANSLATION_LEVEL(),
92    ;
93
94    spec fn PTE_SIZE_spec() -> usize;
95
96    /// The size of a PTE.
97    #[verifier::when_used_as_spec(PTE_SIZE_spec)]
98    fn PTE_SIZE() -> (res: usize)
99        returns
100            Self::PTE_SIZE(),
101    ;
102
103    spec fn ADDRESS_WIDTH_spec() -> usize;
104
105    /// The address width may be BASE_PAGE_SIZE.ilog2() + NR_LEVELS * IN_FRAME_INDEX_BITS.
106    /// If it is shorter than that, the higher bits in the highest level are ignored.
107    #[verifier::when_used_as_spec(ADDRESS_WIDTH_spec)]
108    fn ADDRESS_WIDTH() -> (res: usize)
109        returns
110            Self::ADDRESS_WIDTH(),
111    ;
112
113    spec fn VA_SIGN_EXT_spec() -> bool;
114
115    /// Whether virtual addresses are sign-extended.
116    ///
117    /// The sign bit of a [`Vaddr`] is the bit at index [`PagingConstsTrait::ADDRESS_WIDTH`] - 1.
118    /// If this constant is `true`, bits in [`Vaddr`] that are higher than the sign bit must be
119    /// equal to the sign bit. If an address violates this rule, both the hardware and OSTD
120    /// should reject it.
121    ///
122    /// Otherwise, if this constant is `false`, higher bits must be zero.
123    ///
124    /// Regardless of sign extension, [`Vaddr`] is always not signed upon calculation.
125    /// That means, `0xffff_ffff_ffff_0000 < 0xffff_ffff_ffff_0001` is `true`.
126    #[verifier::when_used_as_spec(VA_SIGN_EXT_spec)]
127    fn VA_SIGN_EXT() -> bool
128        returns
129            Self::VA_SIGN_EXT(),
130    ;
131
132    /// The requirements of the paging constants so that the memory management system can work correctly.
133    ///
134    /// NOTE: The postcondition is designed to be minimal, to actually be used in proofs, call `lemma_paging_consts_properties`
135    /// instead to get all the properties that are derived from the requirements.
136    ///
137    /// FIXME： General architecture support.
138    /// All configs in vostd use the same value for the per-config
139    /// `NR_LEVELS()` as the architecture-level constant `NR_LEVELS`
140    /// (= 4 for x86_64). This is *implicit* in the cursor framework:
141    /// `CursorOwner::inv()` hardcodes `self.level <= NR_LEVELS` (const)
142    /// for cursors over any `C: PagingConstsTrait`, so a config whose
143    /// `NR_LEVELS_spec()` exceeded `NR_LEVELS` would be unusable. This
144    /// lemma exposes that equality as a usable fact so generic proofs
145    /// can chain `level != C::NR_LEVELS_spec()` to `level < NR_LEVELS`
146    /// (e.g. `Cursor::find_next_impl`'s PageTable-branch gate ⟹
147    /// `CursorMut::take_next`'s `replace_cur_entry` discharge).
148    proof fn lemma_paging_consts_requirements()
149        ensures
150            0 < Self::BASE_PAGE_SIZE(),
151            is_pow2(Self::BASE_PAGE_SIZE() as int),
152            Self::NR_LEVELS() > 0,
153            is_pow2(Self::PTE_SIZE() as int),
154            0 < Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
155            0 < Self::ADDRESS_WIDTH() < usize::BITS,
156            Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2()
157                * Self::NR_LEVELS() <= Self::ADDRESS_WIDTH(),
158            Self::PTE_SIZE() == core::mem::size_of::<usize>(),
159            // The following statement holds for all architectures,
160            // but the actual value of the constants may vary.
161            // Maybe we can remove this requirement.
162            Self::BASE_PAGE_SIZE() == PAGE_SIZE,
163            Self::NR_LEVELS() == NR_LEVELS,
164            Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES,
165    ;
166
167    /// The derived properties of the paging constants.
168    ///
169    /// NOTE: Implementations of `PagingConstsTrait` do not need to implement this lemma, the proof is automatically inherited from the default implementation.
170    proof fn lemma_paging_consts_properties()
171        ensures
172    // Derived properties.
173
174            Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * (
175            Self::NR_LEVELS() - 1) <= Self::ADDRESS_WIDTH(),
176            0 < Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
177            NR_ENTRIES * Self::PTE_SIZE() == PAGE_SIZE,
178            // Copied from the postcondition of `lemma_paging_consts_requirements`
179            // so that we only need to call this lemma in proofs.
180            0 < Self::BASE_PAGE_SIZE(),
181            is_pow2(Self::BASE_PAGE_SIZE() as int),
182            Self::NR_LEVELS() > 0,
183            is_pow2(Self::PTE_SIZE() as int),
184            0 < Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
185            0 < Self::ADDRESS_WIDTH() < usize::BITS,
186            Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2()
187                * Self::NR_LEVELS() <= Self::ADDRESS_WIDTH(),
188            Self::PTE_SIZE() == core::mem::size_of::<usize>(),
189            // The following statement holds for all architectures,
190            // but the actual value of the constants may vary.
191            // Maybe we can remove this requirement.
192            Self::BASE_PAGE_SIZE() == PAGE_SIZE,
193            Self::NR_LEVELS() == NR_LEVELS,
194            Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES,
195    {
196        Self::lemma_paging_consts_requirements();
197        broadcast use group_div_basics;
198
199    }
200}
201
202pub open spec fn page_size_spec(level: PagingLevel) -> usize {
203    (PAGE_SIZE * pow2(
204        (nr_subpage_per_huge::<PagingConsts>().ilog2() * (level - 1)) as nat,
205    )) as usize
206}
207
208// /// The page size
209// pub const PAGE_SIZE: usize = page_size::<PagingConsts>(1);
210/// The page size at a given level.
211#[verifier::when_used_as_spec(page_size_spec)]
212pub fn page_size(level: PagingLevel) -> (ret: usize)
213    requires
214        1 <= level <= NR_LEVELS + 1,
215    ensures
216        ret == page_size_spec(level),
217        is_pow2(ret as int),
218        ret >= PAGE_SIZE,
219{
220    proof {
221        let index_bits: usize = nr_subpage_per_huge::<PagingConsts>().ilog2() as usize;
222        PagingConsts::lemma_paging_consts_properties();
223        crate::arch::mm::lemma_nr_subpage_per_huge_eq_nr_entries();
224        vstd::layout::unsigned_int_max_values();
225        vstd::arithmetic::power2::lemma2_to64();
226        vstd::arithmetic::power2::lemma2_to64_rest();
227        vstd_extra::external::ilog2::lemma_usize_pow2_ilog2(9);
228        let level_index: usize = (level - 1) as usize;
229        let shift: usize = (index_bits * level_index) as usize;
230        let ghost shift_nat = shift as nat;
231        let ghost page_shift = 12nat + shift_nat;
232
233        vstd::arithmetic::power2::lemma_pow2_adds(12, shift_nat);
234        if page_shift < 48nat {
235            vstd::arithmetic::power2::lemma_pow2_strictly_increases(page_shift, 48nat);
236        }
237        vstd::bits::lemma_usize_shl_is_mul(PAGE_SIZE, shift);
238        vstd_extra::external::ilog2::lemma_usize_pow2_shl_is_pow2(PAGE_SIZE, shift);
239    }
240    PAGE_SIZE << (nr_subpage_per_huge::<PagingConsts>().ilog2() as usize * (level as usize - 1))
241}
242
243#[verifier::inline]
244pub open spec fn nr_subpage_per_huge_spec<C: PagingConstsTrait>() -> usize {
245    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
246}
247
248/// The number of sub pages in a huge page.
249#[verifier::when_used_as_spec(nr_subpage_per_huge_spec)]
250pub fn nr_subpage_per_huge<C: PagingConstsTrait>() -> (res: usize)
251    ensures
252        res == nr_subpage_per_huge_spec::<C>(),
253{
254    proof {
255        C::lemma_paging_consts_properties();
256    }
257    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
258}
259
260/// The maximum virtual address of user space (non inclusive).
261///
262/// Typical 64-bit systems have at least 48-bit virtual address space.
263/// A typical way to reserve half of the address space for the kernel is
264/// to use the highest 48-bit virtual address space.
265///
266/// Also, the top page is not regarded as usable since it's a workaround
267/// for some x86_64 CPUs' bugs. See
268/// <https://github.com/torvalds/linux/blob/480e035fc4c714fb5536e64ab9db04fedc89e910/arch/x86/include/asm/page_64.h#L68-L78>
269/// for the rationale.
270pub const MAX_USERSPACE_VADDR: Vaddr = 0x0000_8000_0000_0000_usize - PAGE_SIZE;
271
272/// The kernel address space.
273///
274/// There are the high canonical addresses defined in most 48-bit width
275/// architectures.
276pub const KERNEL_VADDR_RANGE: Range<Vaddr> =
277    0xffff_8000_0000_0000_usize..0xffff_ffff_ffff_0000_usize;
278
279/// Gets physical address trait
280pub trait HasPaddr {
281    /// Returns the physical address.
282    fn paddr(&self) -> Paddr;
283}
284
285/// Checks if the given address is page-aligned.
286pub const fn is_page_aligned(p: usize) -> bool {
287    (p & (PAGE_SIZE - 1)) == 0
288}
289
290} // verus!
ostd/mm/mod.rs

ostd/mm/
mod.rs
