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, lemma_div_non_zero};
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() / Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
142            // Copied from the postcondition of `lemma_paging_consts_requirements`
143            // so that we only need to call this lemma in proofs.
144            0 < Self::BASE_PAGE_SIZE(),
145            is_pow2(Self::BASE_PAGE_SIZE() as int),
146            Self::NR_LEVELS() > 0,
147            is_pow2(Self::PTE_SIZE() as int),
148            0 < Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
149            0 < Self::ADDRESS_WIDTH() < usize::BITS,
150            Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * (
151            Self::NR_LEVELS() - 1) <= Self::ADDRESS_WIDTH(),
152            // The following statement holds for all architectures,
153            // but the actual value of the constants may vary.
154            Self::BASE_PAGE_SIZE() == PAGE_SIZE,
155            Self::NR_LEVELS() == NR_LEVELS,
156            Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES,
157    ;
158
159    /// The derived properties of the paging constants.
160    ///
161    /// NOTE: Implementations of `PagingConstsTrait` do not need to implement this lemma, the proof is automatically inherited from the default implementation.
162    proof fn lemma_paging_consts_properties()
163        ensures
164    // Derived properties.
165
166            0 < Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
167            // Copied from the postcondition of `lemma_paging_consts_requirements`
168            // so that we only need to call this lemma in proofs.
169            0 < Self::BASE_PAGE_SIZE(),
170            is_pow2(Self::BASE_PAGE_SIZE() as int),
171            Self::NR_LEVELS() > 0,
172            is_pow2(Self::PTE_SIZE() as int),
173            0 < Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
174            0 < Self::ADDRESS_WIDTH() < usize::BITS,
175            Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * (
176            Self::NR_LEVELS() - 1) <= Self::ADDRESS_WIDTH(),
177            // The following statement holds for all architectures,
178            // but the actual value of the constants may vary.
179            Self::BASE_PAGE_SIZE() == PAGE_SIZE,
180            Self::NR_LEVELS() == NR_LEVELS,
181            Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES,
182    {
183        Self::lemma_paging_consts_requirements();
184        broadcast use group_div_basics;
185
186        assert(Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() > 0) by {
187            lemma_div_non_zero(Self::BASE_PAGE_SIZE() as int, Self::PTE_SIZE() as int);
188        };
189    }
190}
191
192pub open spec fn page_size_spec(level: PagingLevel) -> usize {
193    (PAGE_SIZE * pow2(
194        (nr_subpage_per_huge::<PagingConsts>().ilog2() * (level - 1)) as nat,
195    )) as usize
196}
197
198// /// The page size
199// pub const PAGE_SIZE: usize = page_size::<PagingConsts>(1);
200/// The page size at a given level.
201#[verifier::when_used_as_spec(page_size_spec)]
202#[verifier::external_body]
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    PAGE_SIZE << (nr_subpage_per_huge::<PagingConsts>().ilog2() as usize * (level as usize - 1))
212}
213
214#[verifier::inline]
215pub open spec fn nr_subpage_per_huge_spec<C: PagingConstsTrait>() -> usize {
216    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
217}
218
219/// The number of sub pages in a huge page.
220#[verifier::when_used_as_spec(nr_subpage_per_huge_spec)]
221pub fn nr_subpage_per_huge<C: PagingConstsTrait>() -> (res: usize)
222    ensures
223        res == nr_subpage_per_huge_spec::<C>(),
224{
225    proof {
226        C::lemma_paging_consts_properties();
227    }
228    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
229}
230
231/// The maximum virtual address of user space (non inclusive).
232///
233/// Typical 64-bit systems have at least 48-bit virtual address space.
234/// A typical way to reserve half of the address space for the kernel is
235/// to use the highest 48-bit virtual address space.
236///
237/// Also, the top page is not regarded as usable since it's a workaround
238/// for some x86_64 CPUs' bugs. See
239/// <https://github.com/torvalds/linux/blob/480e035fc4c714fb5536e64ab9db04fedc89e910/arch/x86/include/asm/page_64.h#L68-L78>
240/// for the rationale.
241pub const MAX_USERSPACE_VADDR: Vaddr = 0x0000_8000_0000_0000_usize - PAGE_SIZE;
242
243/// The kernel address space.
244///
245/// There are the high canonical addresses defined in most 48-bit width
246/// architectures.
247pub const KERNEL_VADDR_RANGE: Range<Vaddr> =
248    0xffff_8000_0000_0000_usize..0xffff_ffff_ffff_0000_usize;
249
250/// Gets physical address trait
251pub trait HasPaddr {
252    /// Returns the physical address.
253    fn paddr(&self) -> Paddr;
254}
255
256/// Checks if the given address is page-aligned.
257pub const fn is_page_aligned(p: usize) -> bool {
258    (p & (PAGE_SIZE - 1)) == 0
259}
260
261} // verus!
ostd/mm/mod.rs

ostd/mm/
mod.rs
