ostd/mm/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Virtual memory (VM).
3use crate::specs::arch::PAGE_SIZE;
4use core::fmt::Debug;
5use vstd::arithmetic::div_mod::group_div_basics;
6use vstd::arithmetic::div_mod::lemma_div_non_zero;
7use vstd::arithmetic::power2::*;
8use vstd::prelude::*;
9
10/// Virtual addresses.
11pub type Vaddr = usize;
12
13/// Physical addresses.
14pub type Paddr = usize;
15
16/// The level of a page table node or a frame.
17pub type PagingLevel = u8;
18
19/// The maximum value of `PagingConstsTrait::NR_LEVELS`.
20pub const MAX_NR_LEVELS: usize = 4;
21
22//pub(crate) mod dma;
23pub mod frame;
24//pub mod heap;
25pub mod io;
26pub mod kspace;
27pub(crate) mod page_prop;
28pub mod page_table;
29pub mod pod;
30pub mod tlb;
31pub mod vm_space;
32
33#[cfg(ktest)]
34mod test;
35
36use core::ops::Range;
37
38// Import types and constants from arch
39pub use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, NR_ENTRIES, NR_LEVELS};
40pub use crate::specs::arch::paging_consts::PagingConsts;
41
42// Re-export paddr_to_vaddr from kspace
43pub use kspace::paddr_to_vaddr;
44
45// Re-export largest_pages from page_table
46pub use page_table::largest_pages;
47
48verus! {
49
50/// The maximum virtual address of user space (non inclusive).
51///
52/// Typical 64-bit systems have at least 48-bit virtual address space.
53/// A typical way to reserve half of the address space for the kernel is
54/// to use the highest 48-bit virtual address space.
55///
56/// Also, the top page is not regarded as usable since it's a workaround
57/// for some x86_64 CPUs' bugs. See
58/// <https://github.com/torvalds/linux/blob/480e035fc4c714fb5536e64ab9db04fedc89e910/arch/x86/include/asm/page_64.h#L68-L78>
59/// for the rationale.
60/// Page size.
61pub const MAX_USERSPACE_VADDR: usize = 0x0000_8000_0000_0000 - PAGE_SIZE;
62
63/// The kernel address space.
64///
65/// There are the high canonical addresses defined in most 48-bit width
66/// architectures.
67pub const KERNEL_VADDR_RANGE: Range<Vaddr> = 0xffff_8000_0000_0000..0xffff_ffff_ffff_0000;
68
69/// Gets physical address trait
70pub trait HasPaddr {
71    /// Returns the physical address.
72    fn paddr(&self) -> Paddr;
73}
74
75/// Checks if the given address is page-aligned.
76pub const fn is_page_aligned(p: usize) -> bool {
77    (p & (PAGE_SIZE - 1)) == 0
78}
79
80#[allow(non_snake_case)]
81pub trait PagingConstsTrait: Debug + Sync {
82    spec fn BASE_PAGE_SIZE_spec() -> usize;
83
84    proof fn lemma_BASE_PAGE_SIZE_properties()
85        ensures
86            0 < Self::BASE_PAGE_SIZE_spec(),
87            is_pow2(Self::BASE_PAGE_SIZE_spec() as int),
88    ;
89
90    /// The smallest page size.
91    /// This is also the page size at level 1 page tables.
92    #[verifier::when_used_as_spec(BASE_PAGE_SIZE_spec)]
93    fn BASE_PAGE_SIZE() -> (res: usize)
94        ensures
95            res == Self::BASE_PAGE_SIZE_spec(),
96            0 < res,
97            is_pow2(res as int),
98    ;
99
100    spec fn NR_LEVELS_spec() -> PagingLevel;
101
102    /// The number of levels in the page table.
103    /// The numbering of levels goes from deepest node to the root node. For example,
104    /// the level 1 to 5 on AMD64 corresponds to Page Tables, Page Directory Tables,
105    /// Page Directory Pointer Tables, Page-Map Level-4 Table, and Page-Map Level-5
106    /// Table, respectively.
107    #[verifier::when_used_as_spec(NR_LEVELS_spec)]
108    fn NR_LEVELS() -> (res: PagingLevel)
109        ensures
110            res == Self::NR_LEVELS_spec(),
111            res > 0,
112    ;
113
114    spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel;
115
116    /// The highest level that a PTE can be directly used to translate a VA.
117    /// This affects the the largest page size supported by the page table.
118    #[verifier::when_used_as_spec(HIGHEST_TRANSLATION_LEVEL_spec)]
119    fn HIGHEST_TRANSLATION_LEVEL() -> (res: PagingLevel)
120        ensures
121            res == Self::HIGHEST_TRANSLATION_LEVEL_spec(),
122    ;
123
124    spec fn PTE_SIZE_spec() -> usize;
125
126    /// The size of a PTE.
127    #[verifier::when_used_as_spec(PTE_SIZE_spec)]
128    fn PTE_SIZE() -> (res: usize)
129        ensures
130            res == Self::PTE_SIZE_spec(),
131            is_pow2(res as int),
132            0 < res <= Self::BASE_PAGE_SIZE(),
133    ;
134
135    proof fn lemma_PTE_SIZE_properties()
136        ensures
137            0 < Self::PTE_SIZE_spec() <= Self::BASE_PAGE_SIZE(),
138            is_pow2(Self::PTE_SIZE_spec() as int),
139    ;
140
141    spec fn ADDRESS_WIDTH_spec() -> usize;
142
143    /// The address width may be BASE_PAGE_SIZE.ilog2() + NR_LEVELS * IN_FRAME_INDEX_BITS.
144    /// If it is shorter than that, the higher bits in the highest level are ignored.
145    #[verifier::when_used_as_spec(ADDRESS_WIDTH_spec)]
146    fn ADDRESS_WIDTH() -> (res: usize)
147        ensures
148            res == Self::ADDRESS_WIDTH_spec(),
149    ;
150
151    /// Whether virtual addresses are sign-extended.
152    ///
153    /// The sign bit of a [`Vaddr`] is the bit at index [`PagingConstsTrait::ADDRESS_WIDTH`] - 1.
154    /// If this constant is `true`, bits in [`Vaddr`] that are higher than the sign bit must be
155    /// equal to the sign bit. If an address violates this rule, both the hardware and OSTD
156    /// should reject it.
157    ///
158    /// Otherwise, if this constant is `false`, higher bits must be zero.
159    ///
160    /// Regardless of sign extension, [`Vaddr`] is always not signed upon calculation.
161    /// That means, `0xffff_ffff_ffff_0000 < 0xffff_ffff_ffff_0001` is `true`.
162    spec fn VA_SIGN_EXT_spec() -> bool;
163
164    #[verifier::when_used_as_spec(VA_SIGN_EXT_spec)]
165    fn VA_SIGN_EXT() -> bool;
166}
167
168#[verifier::inline]
169pub open spec fn nr_subpage_per_huge_spec<C: PagingConstsTrait>() -> usize {
170    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
171}
172
173/// The number of sub pages in a huge page.
174#[inline(always)]
175#[verifier::when_used_as_spec(nr_subpage_per_huge_spec)]
176pub fn nr_subpage_per_huge<C: PagingConstsTrait>() -> (res: usize)
177    ensures
178        res == nr_subpage_per_huge_spec::<C>(),
179{
180    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
181}
182
183pub proof fn lemma_nr_subpage_per_huge_bounded<C: PagingConstsTrait>()
184    ensures
185        0 < nr_subpage_per_huge::<C>() <= C::BASE_PAGE_SIZE(),
186{
187    C::lemma_PTE_SIZE_properties();
188    broadcast use group_div_basics;
189
190    assert(C::PTE_SIZE() <= C::BASE_PAGE_SIZE());
191    assert(C::BASE_PAGE_SIZE() / C::PTE_SIZE() <= C::BASE_PAGE_SIZE());
192    assert(C::BASE_PAGE_SIZE() / C::PTE_SIZE() > 0) by {
193        lemma_div_non_zero(C::BASE_PAGE_SIZE() as int, C::PTE_SIZE() as int);
194    };
195}
196
197} // verus!
ostd/mm/mod.rs

ostd/mm/
mod.rs
