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

ostd/mm/kspace/
mod.rs
