ostd/mm/kspace/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Kernel memory space management.
3//!
4//! The kernel memory space is currently managed as follows, if the
5//! address width is 48 bits (with 47 bits kernel space).
6//!
7//! TODO: the cap of linear mapping (the start of vm alloc) are raised
8//! to workaround for high IO in TDX. We need actual vm alloc API to have
9//! a proper fix.
10//!
11//! ```text
12//! +-+ <- the highest used address (0xffff_ffff_ffff_0000)
13//! | |         For the kernel code, 1 GiB.
14//! +-+ <- 0xffff_ffff_8000_0000
15//! | |
16//! | |         Unused hole.
17//! +-+ <- 0xffff_e100_0000_0000
18//! | |         For frame metadata, 1 TiB.
19//! +-+ <- 0xffff_e000_0000_0000
20//! | |         For [`KVirtArea`], 32 TiB.
21//! +-+ <- the middle of the higher half (0xffff_c000_0000_0000)
22//! | |
23//! | |
24//! | |
25//! | |         For linear mappings, 64 TiB.
26//! | |         Mapped physical addresses are untracked.
27//! | |
28//! | |
29//! | |
30//! +-+ <- the base of high canonical address (0xffff_8000_0000_0000)
31//! ```
32//!
33//! If the address width is (according to [`crate::arch::mm::PagingConsts`])
34//! 39 bits or 57 bits, the memory space just adjust proportionally.
35use core::{marker::PhantomData, ops::Range};
36use vstd::atomic::PermissionU64;
37use vstd::prelude::*;
38use vstd::simple_pptr::PointsTo;
39
40//use log::info;
41use crate::sync::{OnceImpl, TrivialPred};
42pub(crate) mod kvirt_area;
43#[cfg(ktest)]
44mod test;
45
46use super::{
47    Paddr, PagingConstsTrait, Vaddr,
48    frame::{
49        Frame, Segment,
50        meta::{AnyFrameMeta, MetaPageMeta, MetaSlot, mapping},
51    },
52    page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags},
53    page_table::{PageTable, PageTableConfig},
54};
55use crate::mm::frame::DynFrame;
56use crate::mm::page_table::RCClone;
57use crate::specs::arch::*;
58use crate::specs::mm::{
59    frame::{
60        mapping::group_page_meta, meta_owners::MetaSlotStorage,
61        meta_region_owners::MetaRegionOwners,
62    },
63    page_table::{nr_pte_index_bits_spec, pte_index_bit_offset_spec},
64};
65use crate::{
66    arch::mm::{PageTableEntry, PagingConsts},
67    boot::memory_region::MemoryRegionType,
68    mm::{PagingLevel, largest_pages},
69    //task::disable_preempt,
70};
71
72use vstd_extra::ownership::*;
73use vstd_extra::prelude::*;
74
75verus! {
76
77/// The shortest supported address width is 39 bits. And the literal
78/// values are written for 48 bits address width. Adjust the values
79/// by arithmetic left shift.
80pub const ADDR_WIDTH_SHIFT: isize = 48 - 48;
81
82/// Start of the kernel address space.
83/// This is the _lowest_ address of the x86-64's _high_ canonical addresses.
84#[cfg(not(target_arch = "loongarch64"))]
85pub const KERNEL_BASE_VADDR: Vaddr = 0xffff_8000_0000_0000 << ADDR_WIDTH_SHIFT;
86
87#[cfg(target_arch = "loongarch64")]
88pub const KERNEL_BASE_VADDR: Vaddr = 0x9000_0000_0000_0000 << ADDR_WIDTH_SHIFT;
89
90/// End of the kernel address space (non inclusive).
91pub const KERNEL_END_VADDR: Vaddr = 0xffff_ffff_ffff_0000 << ADDR_WIDTH_SHIFT;
92
93/*
94/// The kernel code is linear mapped to this address.
95///
96/// FIXME: This offset should be randomly chosen by the loader or the
97/// boot compatibility layer. But we disabled it because OSTD
98/// doesn't support relocatable kernel yet.
99pub fn kernel_loaded_offset() -> usize {
100    KERNEL_CODE_BASE_VADDR
101}*/
102
103#[cfg(target_arch = "x86_64")]
104const KERNEL_CODE_BASE_VADDR: usize = 0xffff_ffff_8000_0000 << ADDR_WIDTH_SHIFT;
105
106#[cfg(target_arch = "riscv64")]
107const KERNEL_CODE_BASE_VADDR: usize = 0xffff_ffff_0000_0000 << ADDR_WIDTH_SHIFT;
108
109#[cfg(target_arch = "loongarch64")]
110const KERNEL_CODE_BASE_VADDR: usize = 0x9000_0000_0000_0000 << ADDR_WIDTH_SHIFT;
111
112pub const FRAME_METADATA_CAP_VADDR: Vaddr = 0xffff_e100_0000_0000 << ADDR_WIDTH_SHIFT;
113
114pub const FRAME_METADATA_BASE_VADDR: Vaddr = 0xffff_e000_0000_0000 << ADDR_WIDTH_SHIFT;
115
116pub const FRAME_METADATA_RANGE: Range<Vaddr> = 0xffff_e000_0000_0000..0xffff_e100_0000_0000;
117
118pub const VMALLOC_BASE_VADDR: Vaddr = 0xffff_c000_0000_0000 << ADDR_WIDTH_SHIFT;
119
120pub const VMALLOC_VADDR_RANGE: Range<Vaddr> = VMALLOC_BASE_VADDR..FRAME_METADATA_BASE_VADDR;
121
122/// The base address of the linear mapping of all physical
123/// memory in the kernel address space.
124pub const LINEAR_MAPPING_BASE_VADDR: Vaddr = 0xffff_8000_0000_0000 << ADDR_WIDTH_SHIFT;
125
126pub const LINEAR_MAPPING_VADDR_RANGE: Range<Vaddr> = LINEAR_MAPPING_BASE_VADDR..VMALLOC_BASE_VADDR;
127
128/*
129#[cfg(not(target_arch = "loongarch64"))]
130pub const LINEAR_MAPPING_BASE_VADDR: Vaddr = 0xffff_8000_0000_0000 << ADDR_WIDTH_SHIFT;
131#[cfg(target_arch = "loongarch64")]
132pub const LINEAR_MAPPING_BASE_VADDR: Vaddr = 0x9000_0000_0000_0000 << ADDR_WIDTH_SHIFT;
133pub const LINEAR_MAPPING_VADDR_RANGE: Range<Vaddr> = LINEAR_MAPPING_BASE_VADDR..VMALLOC_BASE_VADDR;
134*/
135
136/// Convert physical address to virtual address using offset, only available inside `ostd`
137pub open spec fn paddr_to_vaddr_spec(pa: Paddr) -> usize {
138    (pa + LINEAR_MAPPING_BASE_VADDR) as usize
139}
140
141#[verifier::when_used_as_spec(paddr_to_vaddr_spec)]
142pub fn paddr_to_vaddr(pa: Paddr) -> usize
143    requires
144        pa + LINEAR_MAPPING_BASE_VADDR < usize::MAX,
145    returns
146        paddr_to_vaddr_spec(pa),
147{
148    //debug_assert!(pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR);
149    pa + LINEAR_MAPPING_BASE_VADDR
150}
151
152/// The kernel page table instance.
153///
154/// It manages the kernel mapping of all address spaces by sharing the kernel part. And it
155/// is unlikely to be activated.
156#[allow(private_interfaces)]
157pub exec static KERNEL_PAGE_TABLE: OnceImpl<PageTable<KernelPtConfig>, TrivialPred> = OnceImpl::new(
158    Ghost(TrivialPred),
159);
160
161#[verifier::allow(autoderive_clone_without_spec)]
162#[derive(Clone, Debug)]
163pub(crate) struct KernelPtConfig {}
164
165// We use the first available PTE bit to mark the frame as tracked.
166// SAFETY: `item_into_raw` and `item_from_raw` are implemented correctly,
167unsafe impl PageTableConfig for KernelPtConfig {
168    open spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize> {
169        256..512
170    }
171
172    open spec fn LEADING_BITS_spec() -> usize {
173        0xffff
174    }
175
176    proof fn lemma_page_table_config_constant_requirements() {
177        use crate::mm::nr_subpage_per_huge;
178        use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2};
179        Self::C::lemma_paging_consts_properties();
180        PageTableEntry::lemma_layout();
181        lemma2_to64();
182        lemma2_to64_rest();
183        vstd::layout::unsigned_int_max_values();
184        lemma_usize_pow2_ilog2(12);
185        lemma_usize_pow2_ilog2(9);
186        lemma_pow2_adds(9, 39);
187        lemma_pow2_adds(8, 39);
188
189        assert((256 * pow2(39) as int) / (pow2(47) as int) == 1);
190        lemma_pow2_adds(16, 48);
191    }
192
193    fn TOP_LEVEL_INDEX_RANGE() -> (r: Range<usize>) {
194        256..512
195    }
196
197    open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool {
198        false
199    }
200
201    fn TOP_LEVEL_CAN_UNMAP() -> (b: bool) {
202        false
203    }
204
205    // The kvirt allocator (the only source of kernel-PT cursor ranges) caps
206    // `range.end` at FRAME_METADATA_BASE_VADDR — see `kvirt_alloc_range_bounds`.
207    open spec fn LOCKED_END_BOUND_spec() -> int {
208        FRAME_METADATA_BASE_VADDR as int
209    }
210
211    type E = PageTableEntry;
212
213    type C = PagingConsts;
214
215    type Item = MappedItem;
216
217    open spec fn item_into_raw_spec(item: Self::Item) -> (Paddr, PagingLevel, PageProperty) {
218        match item {
219            MappedItem::Tracked(frame, prop) => (
220                crate::mm::frame::meta::mapping::meta_to_frame(frame.ptr.addr()),
221                1,
222                Self::encode_tracked_prop(prop),
223            ),
224            MappedItem::Untracked(pa, level, prop) => (pa, level, Self::decode_tracked_prop(prop)),
225        }
226    }
227
228    #[verifier::external_body]
229    fn item_into_raw(item: Self::Item) -> (res: (Paddr, PagingLevel, PageProperty)) {
230        match item {
231            MappedItem::Tracked(frame, mut prop) => {
232                debug_assert!(!prop.flags.contains(PageFlags::AVAIL1()));
233                prop.flags = prop.flags | PageFlags::AVAIL1();
234                let level = frame.map_level();
235                let paddr = frame.into_raw();
236                (paddr, level, prop)
237            },
238            MappedItem::Untracked(pa, level, mut prop) => {
239                debug_assert!(!prop.flags.contains(PageFlags::AVAIL1()));
240                prop.flags = prop.flags - PageFlags::AVAIL1();
241                (pa, level, prop)
242            },
243        }
244    }
245
246    open spec fn item_from_raw_spec(
247        paddr: Paddr,
248        level: PagingLevel,
249        prop: PageProperty,
250    ) -> Self::Item {
251        if prop.flags.contains(PageFlags::AVAIL1()) {
252            MappedItem::Tracked(
253                Frame::<MetaSlotStorage> {
254                    ptr: vstd::simple_pptr::PPtr(mapping::frame_to_meta(paddr), PhantomData),
255                    _marker: PhantomData,
256                },
257                Self::decode_tracked_prop(prop),
258            )
259        } else {
260            MappedItem::Untracked(paddr, level, prop)
261        }
262    }
263
264    #[verifier::external_body]
265    unsafe fn item_from_raw(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> Self::Item {
266        if prop.flags.contains(PageFlags::AVAIL1()) {
267            debug_assert_eq!(level, 1);
268            // [KNOWN] BUG FOUND BY FV: forgotting to clean `AVAIL1`. https://github.com/asterinas/vostd/issues/625
269            let mut item_prop = prop;
270            item_prop.flags = item_prop.flags - PageFlags::AVAIL1();
271            // SAFETY: The caller ensures safety.
272            let frame = unsafe { Frame::<MetaSlotStorage>::from_raw(paddr) };
273            MappedItem::Tracked(frame, item_prop)
274        } else {
275            MappedItem::Untracked(paddr, level, prop)
276        }
277    }
278
279    proof fn lemma_item_into_raw_roundtrip(pa: Paddr, level: PagingLevel, prop: PageProperty) {
280        broadcast use group_page_meta;
281
282        assert(Self::raw_item_well_formed(pa, level, prop));
283        Self::lemma_item_from_raw_well_formed(pa, level, prop);
284        prop.lemma_avail1_tag_encoding();
285    }
286
287    proof fn lemma_item_from_raw_roundtrip(
288        item: Self::Item,
289        paddr: Paddr,
290        level: PagingLevel,
291        prop: PageProperty,
292    ) {
293        broadcast use group_page_meta;
294
295        match item {
296            MappedItem::Tracked(frame, prop_actual) => {
297                assert(Self::item_well_formed(item));
298                prop_actual.lemma_avail1_tag_encoding();
299            },
300            MappedItem::Untracked(_, _, prop_actual) => {
301                assert(Self::item_well_formed(item));
302                prop_actual.lemma_avail1_tag_encoding();
303            },
304        }
305    }
306
307    open spec fn tracked(item: Self::Item) -> bool {
308        // Tracked items hold a reference; clone bumps rc. Untracked items
309        // (MMIO frames) are not ref-counted; clone is a no-op.
310        item is Tracked
311    }
312
313    open spec fn item_well_formed(item: Self::Item) -> bool {
314        match item {
315            MappedItem::Tracked(frame, prop) => {
316                &&& !prop.flags.contains(PageFlags::AVAIL1())
317                &&& frame.inv()
318            },
319            MappedItem::Untracked(_, _, prop) => !prop.flags.contains(PageFlags::AVAIL1()),
320        }
321    }
322
323    open spec fn raw_item_well_formed(_pa: Paddr, level: PagingLevel, prop: PageProperty) -> bool {
324        prop.flags.contains(PageFlags::AVAIL1()) ==> level == 1
325    }
326
327    proof fn lemma_raw_item_well_formed_preserved(
328        pa: Paddr,
329        level: PagingLevel,
330        old_prop: PageProperty,
331        new_prop: PageProperty,
332    ) {
333    }
334
335    proof fn lemma_raw_item_well_formed_split(
336        pa: Paddr,
337        level: PagingLevel,
338        prop: PageProperty,
339        child_pa: Paddr,
340        child_idx: usize,
341    ) {
342        assert(<PageTableEntry as crate::mm::page_table::PageTableEntryTrait>::new_page_req(
343            pa,
344            level,
345            prop,
346        ));
347        assert(<PageTableEntry as crate::mm::page_table::PageTableEntryTrait>::new_page_req(
348            child_pa,
349            (level - 1) as PagingLevel,
350            prop,
351        ));
352    }
353
354    proof fn lemma_item_from_raw_well_formed(pa: Paddr, level: PagingLevel, prop: PageProperty) {
355        broadcast use group_page_meta;
356
357        prop.lemma_avail1_tag_encoding();
358        if prop.flags.contains(PageFlags::AVAIL1()) {
359            let item = Self::item_from_raw_spec(pa, level, prop);
360            assert(Self::item_well_formed(item));
361        } else {
362            let item = Self::item_from_raw_spec(pa, level, prop);
363            assert(Self::item_well_formed(item));
364        }
365    }
366
367    proof fn lemma_clone_ensures_concrete(
368        item: Self::Item,
369        pa: Paddr,
370        old_regions: MetaRegionOwners,
371        new_regions: MetaRegionOwners,
372        res: Self::Item,
373    ) {
374        use crate::specs::mm::frame::mapping::meta_to_index;
375
376        match item {
377            MappedItem::Tracked(frame, _) => {
378                let frame_idx = meta_to_index(frame.ptr.addr());
379                assert(<MappedItem as RCClone>::clone_ensures(item, old_regions, new_regions, res));
380            },
381            MappedItem::Untracked(_, _, _) => {},
382        }
383    }
384
385    proof fn lemma_clone_requires_concrete(
386        item: Self::Item,
387        pa: Paddr,
388        level: PagingLevel,
389        prop: PageProperty,
390        regions: MetaRegionOwners,
391    ) {
392        use crate::mm::frame::meta::mapping::meta_to_frame;
393        broadcast use group_page_meta;
394
395        Self::lemma_item_from_raw_well_formed(pa, level, prop);
396    }
397}
398
399impl KernelPtConfig {
400    /// Adds the raw PTE bit used to identify a ref-counted mapping.
401    pub open spec fn encode_tracked_prop(prop: PageProperty) -> PageProperty {
402        PageProperty { flags: prop.flags.union(PageFlags::AVAIL1()), ..prop }
403    }
404
405    /// Removes the raw PTE trackedness bit from a caller-visible property.
406    pub open spec fn decode_tracked_prop(prop: PageProperty) -> PageProperty {
407        PageProperty { flags: prop.flags.difference(PageFlags::AVAIL1()), ..prop }
408    }
409}
410
411/*
412#[derive(Clone, Debug, PartialEq, Eq)]
413pub(crate) enum MappedItem {
414    Tracked(Frame<dyn AnyFrameMeta>, PageProperty),
415    Untracked(Paddr, PagingLevel, PageProperty),
416}
417*/
418
419pub enum MappedItem {
420    Tracked(DynFrame, PageProperty),
421    Untracked(Paddr, PagingLevel, PageProperty),
422}
423
424impl RCClone for MappedItem {
425    open spec fn clone_requires(self, perm: MetaRegionOwners) -> bool {
426        match self {
427            MappedItem::Tracked(frame, _) => frame.clone_requires(perm),
428            MappedItem::Untracked(_, _, _) => perm.inv(),
429        }
430    }
431
432    open spec fn clone_ensures(
433        self,
434        old_perm: MetaRegionOwners,
435        new_perm: MetaRegionOwners,
436        res: Self,
437    ) -> bool {
438        match (self, res) {
439            (
440                MappedItem::Tracked(frame, _),
441                MappedItem::Tracked(res_frame, _),
442            ) => frame.clone_ensures(old_perm, new_perm, res_frame),
443            (MappedItem::Untracked(_, _, _), _) => old_perm == new_perm,
444            _ => true,
445        }
446    }
447
448    #[verifier::external_body]
449    fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> (res: Self) {
450        unimplemented!();
451    }
452}
453
454} // verus!
455// /// Initializes the kernel page table.
456// ///
457// /// This function should be called after:
458// ///  - the page allocator and the heap allocator are initialized;
459// ///  - the memory regions are initialized.
460// ///
461// /// This function should be called before:
462// ///  - any initializer that modifies the kernel page table.
463// pub fn init_kernel_page_table(meta_pages: Segment<MetaPageMeta>) {
464//     info!("Initializing the kernel page table");
465//     // Start to initialize the kernel page table.
466//     let kpt = PageTable::<KernelPtConfig>::new_kernel_page_table();
467//     let preempt_guard = disable_preempt();
468//     // In LoongArch64, we don't need to do linear mappings for the kernel because of DMW0.
469//     #[cfg(not(target_arch = "loongarch64"))]
470//     // Do linear mappings for the kernel.
471//     {
472//         let max_paddr = crate::mm::frame::max_paddr();
473//         let from = LINEAR_MAPPING_BASE_VADDR..LINEAR_MAPPING_BASE_VADDR + max_paddr;
474//         let prop = PageProperty {
475//             flags: PageFlags::RW,
476//             cache: CachePolicy::Writeback,
477//             priv_flags: PrivilegedPageFlags::GLOBAL,
478//         };
479//         let mut cursor = kpt.cursor_mut(&preempt_guard, &from).unwrap();
480//         for (pa, level) in largest_pages::<KernelPtConfig>(from.start, 0, max_paddr) {
481//             // SAFETY: we are doing the linear mapping for the kernel.
482//             unsafe { cursor.map(MappedItem::Untracked(pa, level, prop)) }
483//                 .expect("Kernel linear address space is mapped twice");
484//         }
485//     }
486//     // Map the metadata pages.
487//     {
488//         let start_va = mapping::frame_to_meta::<PagingConsts>(0);
489//         let from = start_va..start_va + meta_pages.size();
490//         let prop = PageProperty {
491//             flags: PageFlags::RW,
492//             cache: CachePolicy::Writeback,
493//             priv_flags: PrivilegedPageFlags::GLOBAL,
494//         };
495//         let mut cursor = kpt.cursor_mut(&preempt_guard, &from).unwrap();
496//         // We use untracked mapping so that we can benefit from huge pages.
497//         // We won't unmap them anyway, so there's no leaking problem yet.
498//         // TODO: support tracked huge page mapping.
499//         let pa_range = meta_pages.into_raw();
500//         for (pa, level) in
501//             largest_pages::<KernelPtConfig>(from.start, pa_range.start, pa_range.len())
502//         {
503//             // SAFETY: We are doing the metadata mappings for the kernel.
504//             unsafe { cursor.map(MappedItem::Untracked(pa, level, prop)) }
505//                 .expect("Frame metadata address space is mapped twice");
506//         }
507//     }
508//     // In LoongArch64, we don't need to do linear mappings for the kernel code because of DMW0.
509//     #[cfg(not(target_arch = "loongarch64"))]
510//     // Map for the kernel code itself.
511//     // TODO: set separated permissions for each segments in the kernel.
512//     {
513//         let regions = &crate::boot::EARLY_INFO.get().unwrap().memory_regions;
514//         let region = regions
515//             .iter()
516//             .find(|r| r.typ() == MemoryRegionType::Kernel)
517//             .unwrap();
518//         let offset = kernel_loaded_offset();
519//         let from = region.base() + offset..region.end() + offset;
520//         let prop = PageProperty {
521//             flags: PageFlags::RWX,
522//             cache: CachePolicy::Writeback,
523//             priv_flags: PrivilegedPageFlags::GLOBAL,
524//         };
525//         let mut cursor = kpt.cursor_mut(&preempt_guard, &from).unwrap();
526//         for (pa, level) in largest_pages::<KernelPtConfig>(from.start, region.base(), from.len()) {
527//             // SAFETY: we are doing the kernel code mapping.
528//             unsafe { cursor.map(MappedItem::Untracked(pa, level, prop)) }
529//                 .expect("Kernel code mapped twice");
530//         }
531//     }
532//     KERNEL_PAGE_TABLE.call_once(|| kpt);
533// }
534// /// Activates the kernel page table.
535// ///
536// /// # Safety
537// ///
538// /// This function should only be called once per CPU.
539// pub unsafe fn activate_kernel_page_table() {
540//     let kpt = KERNEL_PAGE_TABLE
541//         .get()
542//         .expect("The kernel page table is not initialized yet");
543//     // SAFETY: the kernel page table is initialized properly.
544//     unsafe {
545//         kpt.first_activate_unchecked();
546//         crate::arch::mm::tlb_flush_all_including_global();
547//     }
548//     // SAFETY: the boot page table is OK to be dismissed now since
549//     // the kernel page table is activated just now.
550//     unsafe {
551//         crate::mm::page_table::boot_pt::dismiss();
552//     }
553// }
ostd/mm/kspace/mod.rs

ostd/mm/kspace/
mod.rs
