ostd/mm/
mod.rs

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

ostd/mm/
mod.rs
