ostd/mm/
mod.rs

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

ostd/mm/
mod.rs
