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

ostd/mm/
mod.rs
