Skip to main content

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