ostd/mm/page_table/node/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2//! This module defines page table node abstractions and the handle.
3//!
4//! The page table node is also frequently referred to as a page table in many architectural
5//! documentations. It is essentially a page that contains page table entries (PTEs) that map
6//! to child page tables nodes or mapped pages.
7//!
8//! This module leverages the page metadata to manage the page table pages, which makes it
9//! easier to provide the following guarantees:
10//!
11//! The page table node is not freed when it is still in use by:
12//!    - a parent page table node,
13//!    - or a handle to a page table node,
14//!    - or a processor.
15//!
16//! This is implemented by using a reference counter in the page metadata. If the above
17//! conditions are not met, the page table node is ensured to be freed upon dropping the last
18//! reference.
19//!
20//! One can acquire exclusive access to a page table node using merely the physical address of
21//! the page table node. This is implemented by a lock in the page metadata. Here the
22//! exclusiveness is only ensured for kernel code, and the processor's MMU is able to access the
23//! page table node while a lock is held. So the modification to the PTEs should be done after
24//! the initialization of the entity that the PTE points to. This is taken care in this module.
25//!
26mod child;
27mod entry;
28
29#[path = "../../../../specs/mm/page_table/node/child.rs"]
30mod child_specs;
31#[path = "../../../../specs/mm/page_table/node/entry.rs"]
32mod entry_specs;
33
34use vstd::{atomic::PAtomicU8, cell::pcell_maybe_uninit, prelude::*, simple_pptr::PPtr};
35use vstd_extra::{array_ptr, cast_ptr::*, ghost_tree::*, ownership::*};
36
37pub use crate::specs::mm::page_table::node::{entry_owners::*, owners::*};
38use crate::specs::mm::{
39    frame::{
40        mapping::{frame_to_index, lemma_frame_to_index_injective, meta_to_index},
41        meta_owners::{
42            FracMetadataPerm, MetaSlotOwner, MetadataPerm, typed_meta_value, typed_meta_wf,
43        },
44        meta_region_owners::MetaRegionOwners,
45    },
46    page_table::node::owners::*,
47};
48
49use super::{PageTableConfig, PageTableEntryTrait, nr_subpage_per_huge};
50use crate::mm::frame::{
51    allocator::FrameAllocOptions,
52    meta::{
53        META_SLOT_SIZE, MetaSlot, REF_COUNT_MAX, REF_COUNT_UNUSED,
54        mapping::{frame_to_meta, meta_to_frame},
55    },
56};
57use crate::mm::page_table::*;
58use crate::mm::{Paddr, Vaddr};
59use crate::{
60    mm::{
61        PagingConstsTrait,
62        PagingLevel,
63        //        FrameAllocOptions, Infallible,
64        //        VmReader,
65        frame::{Frame, FrameRef, meta::AnyFrameMeta},
66        paddr_to_vaddr,
67        page_table::{load_pte, store_pte},
68    },
69    specs::task::InAtomicMode,
70};
71pub use child::*;
72use core::{marker::PhantomData, ops::Deref, sync::atomic::Ordering};
73pub use entry::*;
74
75verus! {
76
77/// The metadata of any kinds of page table pages.
78/// Make sure the the generic parameters don't effect the memory layout.
79pub struct PageTablePageMeta<C: PageTableConfig> {
80    /// The number of valid PTEs. It is mutable if the lock is held.
81    pub nr_children: pcell_maybe_uninit::PCell<u16>,
82    /// If the page table is detached from its parent.
83    ///
84    /// A page table can be detached from its parent while still being accessed,
85    /// since we use a RCU scheme to recycle page tables. If this flag is set,
86    /// it means that the parent is recycling the page table.
87    pub stray: pcell_maybe_uninit::PCell<bool>,
88    /// The level of the page table page. A page table page cannot be
89    /// referenced by page tables of different levels.
90    pub level: PagingLevel,
91    /// The lock for the page table page.
92    pub lock: PAtomicU8,
93    pub _phantom: core::marker::PhantomData<C>,
94}
95
96/// A smart pointer to a page table node.
97///
98/// This smart pointer is an owner of a page table node. Thus creating and
99/// dropping it will affect the reference count of the page table node. If
100/// dropped it as the last reference, the page table node and subsequent
101/// children will be freed.
102///
103/// [`PageTableNode`] is read-only. To modify the page table node, lock and use
104/// [`PageTableGuard`].
105pub type PageTableNode<C> = Frame<PageTablePageMeta<C>>;
106
107unsafe impl<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C> {
108    /// Caller invariants the PT-node `on_drop` body relies on:
109    /// - Reader well-formedness + `vm_io_owner` matching + read view
110    ///   initialized + at least `PAGE_SIZE` bytes remaining for the
111    ///   PT-node walk.
112    /// - Global region table invariant.
113    /// - Embedding ([`child_perms_embedding`]): for every paddr in
114    ///   `child_perms.dom()`, the slot and perm match `from_raw` /
115    ///   `VerifiedDrop::drop`'s expected shape.
116    /// - Walk coverage ([`walk_coverage_from_view`]): for every present
117    ///   non-last PTE in the page bytes, `frame_to_index(pte.paddr()) ∈
118    ///   child_perms.dom()`.
119    /// - Walk uniqueness ([`walk_uniqueness_from_view`]): distinct PTE
120    ///   positions with present non-last PTEs have distinct paddrs.
121    ///
122    /// Coverage and uniqueness retain the memory-safety premises needed by the
123    /// trusted destructor body, without storing item permissions in
124    /// [`VmIoOwner`](crate::specs::mm::io::VmIoOwner).
125    open spec fn on_drop_pre(
126        &self,
127        reader: crate::mm::VmReader<'_, crate::mm::Infallible>,
128        regions: crate::specs::mm::frame::meta_region_owners::MetaRegionOwners,
129        vm_io_owner: crate::specs::mm::io::VmIoOwner,
130    ) -> bool {
131        &&& reader.inv()
132        &&& reader.wf(vm_io_owner)
133        &&& reader.remain_spec() >= crate::specs::arch::PAGE_SIZE
134        &&& reader.cursor.vaddr % core::mem::align_of::<C::E>() == 0
135        &&& vm_io_owner.inv()
136        &&& vm_io_owner.read_view_initialized()
137        &&& regions.inv()
138        &&& Self::child_perms_embedding(regions, vstd::set::Set::empty())
139        &&& self.walk_coverage_from_view(reader, vm_io_owner.read_view_of(), regions.slots.dom())
140        &&& self.walk_uniqueness_from_view(reader, vm_io_owner.read_view_of())
141    }
142
143    /// Drops the children of a page-table node.
144    ///
145    /// The permission handoff for recursively destroying page-table entries is
146    /// not modeled yet. Keep that trusted boundary local to this destructor;
147    /// `VmIoOwner` only supplies the memory view used by `reader`.
148    #[verifier::external_body]
149    fn on_drop(
150        &mut self,
151        reader: &mut crate::mm::VmReader<'_, crate::mm::Infallible>,
152        Tracked(regions): Tracked<
153            &mut crate::specs::mm::frame::meta_region_owners::MetaRegionOwners,
154        >,
155        Tracked(_vm_io_owner): Tracked<&mut crate::specs::mm::io::VmIoOwner>,
156    ) {
157        let level = self.level;
158        let range = if level == C::NR_LEVELS() {
159            C::TOP_LEVEL_INDEX_RANGE()
160        } else {
161            0..nr_subpage_per_huge::<C>()
162        };
163
164        reader.skip_in_place(range.start * core::mem::size_of::<C::E>());
165
166        let mut i = range.start;
167        while i < range.end {
168            // Non-atomic read is OK because we have mutable access.
169            let pte = reader.read_once::<C::E>().unwrap();
170            if pte.is_present() {
171                let paddr = pte.paddr();
172                // As a fast path, we can ensure that the type of the child frame
173                // is `Self` if the PTE points to a child page table. Then we don't
174                // need to check the vtable for the drop method.
175                if !pte.is_last(level) {
176                    // SAFETY: The PTE points to a page table node. The ownership
177                    // of the child is transferred to the child then dropped.
178                    let frame = unsafe { Frame::<Self>::from_raw(paddr) };
179                    frame.drop(Tracked(regions));
180                } else {
181                    proof_decl! {
182                        let tracked item_perm: Option<C::Perm>;
183                    }
184                    // SAFETY: The PTE points to a mapped item. The ownership
185                    // of the item is transferred here then dropped.
186                    let _item = unsafe {
187                        C::item_from_raw(paddr, level, pte.prop(), Tracked(item_perm))
188                    };
189                }
190            }
191            i += 1;
192        }
193    }
194
195    fn is_untyped(&self) -> bool {
196        false
197    }
198
199    uninterp spec fn vtable_ptr(&self) -> usize;
200}
201
202#[verus_verify]
203impl<C: PageTableConfig> PageTableNode<C> {
204    /// Gets the level of a page table node.
205    /// # Verified Properties
206    /// ## Preconditions
207    /// - The node must be well-formed, and the caller must provide a permission token for its metadata.
208    /// ## Postconditions
209    /// - Returns the level of the node.
210    /// ## Safety
211    /// - We require the caller to provide a permission token to ensure that this function is only called on a valid page table node.
212    #[verus_spec(
213        with
214            Tracked(owner): Tracked<&NodeOwner<C>>,
215    )]
216    pub(super) fn level(&self) -> PagingLevel
217        requires
218            self.external_meta_wf(owner.frame_permission.resource(), ()),
219        returns
220            owner.level(),
221    {
222        #[verus_spec(with
223            Tracked(Some(owner.tracked_borrow_metadata_perm())),
224            Tracked(&())
225        )]
226        let meta = self.meta();
227        meta.level
228    }
229
230    /// Allocates a new empty page table node.
231    #[verus_spec(res =>
232        with Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
233             Tracked(regions): Tracked<&mut MetaRegionOwners>,
234             Tracked(guards): Tracked<&Guards>,
235             Ghost(idx): Ghost<usize>,
236                 -> owner: Tracked<OwnerSubtree<C>>,
237        requires
238            1 <= level < NR_LEVELS,
239            idx < NR_ENTRIES,
240            old(regions).inv(),
241            old(parent_owner).inv(),
242        ensures
243            final(regions).inv(),
244            final(parent_owner).inv(),
245            allocated_empty_node_owner(owner@, level),
246            allocated_empty_node_grandchildren_none(owner@),
247            res.ptr.addr() == owner@.value().node().slot_vaddr(),
248            res.inv(),
249            res.wf_with_region(*final(regions)),
250            guards.unlocked(owner@.value().node().slot_vaddr()),
251            MetaSlot::get_node_from_unused_spec(meta_to_frame(owner@.value().node().slot_vaddr()), *old(regions), *final(regions)),
252            MetaSlot::slot_perm_reparked_spec(meta_to_frame(owner@.value().node().slot_vaddr()), *old(regions), *final(regions)),
253
254            old(regions).contains(meta_to_index(owner@.value().node().slot_vaddr())),
255
256            !crate::specs::mm::frame::meta_owners::is_mmio_paddr(
257                meta_to_frame(owner@.value().node().slot_vaddr())),
258            owner@.value().metaregion_sound(*final(regions)),
259            forall|i: int|
260                #[trigger] old(regions).ref_count(i) != REF_COUNT_UNUSED
261                ==> i != meta_to_index(owner@.value().node().slot_vaddr()),
262            owner@.value().match_pte(C::E::new_pt_spec(meta_to_frame(owner@.value().node().slot_vaddr())), level as PagingLevel),
263            final(parent_owner).meta_own == old(parent_owner).meta_own,
264            final(parent_owner).frame_permission == old(parent_owner).frame_permission,
265            final(parent_owner).slot_index == old(parent_owner).slot_index,
266            final(parent_owner).level() == old(parent_owner).level(),
267            final(parent_owner).tree_level == old(parent_owner).tree_level,
268            final(parent_owner).children_perm.addr() == old(parent_owner).children_perm.addr(),
269            final(parent_owner).children_perm.value() == old(parent_owner).children_perm.value().update(
270                idx as int,
271                C::E::new_pt_spec(meta_to_frame(owner@.value().node().slot_vaddr())),
272            ),
273            final(regions).contains(owner@.value().node().slot_index),
274            owner@.value().node().metaregion_sound_node(*final(regions)),
275    )]
276    #[verifier::external_body]
277    pub fn alloc<'rcu>(level: PagingLevel) -> Self {
278        let tracked entry_owner = EntryOwner::tracked_new_absent(
279            TreePath::new(Seq::empty()),
280            level,
281        );
282
283        let tracked mut owner = OwnerSubtree::<C>::tracked_new_val(entry_owner, level as nat);
284        let meta = PageTablePageMeta::new(level);
285        let mut frame = FrameAllocOptions::new();
286        frame.zeroed(true);
287        let allocated_frame = frame.alloc_frame_with(meta).expect(
288            "Failed to allocate a page table node",
289        );
290        // The allocated frame is zeroed. Make sure zero is absent PTE.
291        //debug_assert_eq!(C::E::new_absent().as_usize(), 0);
292
293        proof_with!(|= Tracked(owner));
294
295        allocated_frame
296    }/*
297    /// Activates the page table assuming it is a root page table.
298    ///
299    /// Here we ensure not dropping an active page table by making a
300    /// processor a page table owner. When activating a page table, the
301    /// reference count of the last activated page table is decremented.
302    /// And that of the current page table is incremented.
303    ///
304    /// # Safety
305    ///
306    /// The caller must ensure that the page table to be activated has
307    /// proper mappings for the kernel and has the correct const parameters
308    /// matching the current CPU.
309    ///
310    /// # Panics
311    ///
312    /// Only top-level page tables can be activated using this function.
313    pub(crate) unsafe fn activate(&self) {
314        use crate::{
315            arch::mm::{activate_page_table, current_page_table_paddr},
316            mm::page_prop::CachePolicy,
317        };
318
319        #[cfg(feature = "allow_panic")]
320        assert_eq!(self.level(), C::NR_LEVELS());
321
322        let last_activated_paddr = current_page_table_paddr();
323        if last_activated_paddr == self.start_paddr() {
324            return;
325        }
326
327        // SAFETY: The safety is upheld by the caller.
328        unsafe { activate_page_table(self.clone().into_raw(), CachePolicy::Writeback) };
329
330        // Restore and drop the last activated page table.
331        // SAFETY: The physical address is valid and points to a forgotten page table node.
332        drop(unsafe { Self::from_raw(last_activated_paddr) });
333    }
334
335    /// Activates the (root) page table assuming it is the first activation.
336    ///
337    /// It will not try dropping the last activate page table. It is the same
338    /// with [`Self::activate()`] in other senses.
339    pub(super) unsafe fn first_activate(&self) {
340        use crate::{arch::mm::activate_page_table, mm::page_prop::CachePolicy};
341
342        // SAFETY: The safety is upheld by the caller.
343        unsafe { activate_page_table(self.clone().into_raw(), CachePolicy::Writeback) };
344    }*/
345
346}
347
348#[verus_verify]
349impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C> {
350    pub open spec fn locks_preserved_except<'rcu>(
351        addr: usize,
352        guards0: Guards,
353        guards1: Guards,
354    ) -> bool {
355        &&& OwnerSubtree::implies(
356            CursorOwner::<'rcu, C>::node_unlocked(guards0),
357            CursorOwner::<'rcu, C>::node_unlocked_except(guards1, addr),
358        )
359        &&& forall|i: usize| guards0.lock_held(i) ==> guards1.lock_held(i)
360        &&& forall|i: usize| guards0.unlocked(i) && i != addr ==> guards1.unlocked(i)
361    }
362
363    /// Locks the page table node.
364    ///
365    /// An atomic mode guard is required to
366    ///  1. prevent deadlocks;
367    ///  2. provide a lifetime (`'rcu`) that the nodes are guaranteed to outlive.
368    /// # Verification Design
369    /// As of when we verified this library, we didn't have a spin lock implementation, so we axiomatize
370    /// what happens when it's successful.
371    #[verifier::external_body]
372    #[verus_spec(res =>
373        with Tracked(owner): Tracked<&NodeOwner<C>>,
374            Tracked(guards): Tracked<&mut Guards>
375        requires
376            self.inner@.invariants(*owner),
377            self.inner@.external_meta_wf(owner.frame_permission.resource(), ()),
378            old(guards).unlocked(owner.slot_vaddr()),
379        ensures
380            final(guards).lock_held(owner.slot_vaddr()),
381            Self::locks_preserved_except(owner.slot_vaddr(), *old(guards), *final(guards)),
382            owner.relate_guard(res),
383    )]
384    pub fn lock<'rcu, A: InAtomicMode>(self, _guard: &'rcu A) -> PageTableGuard<'rcu, C> where
385        'a: 'rcu,
386     {
387        unimplemented!()
388    }
389
390    /// Creates a new [`PageTableGuard`] without checking if the page table lock is held.
391    ///
392    /// # Safety
393    ///
394    /// This function must be called if this task logically holds the lock.
395    ///
396    /// Calling this function when a guard is already created is undefined behavior
397    /// unless that guard was already forgotten.
398    #[verus_spec(res =>
399        with Tracked(owner): Tracked<&NodeOwner<C>>,
400             Tracked(guards): Tracked<&mut Guards>,
401        requires
402            self.inner@.invariants(*owner),
403            self.inner@.external_meta_wf(owner.frame_permission.resource(), ()),
404            old(guards).unlocked(owner.slot_vaddr()),
405        ensures
406            final(guards).lock_held(owner.slot_vaddr()),
407            Self::locks_preserved_except(owner.slot_vaddr(), *old(guards), *final(guards)),
408            owner.relate_guard(res),
409    )]
410    pub unsafe fn make_guard_unchecked<'rcu, A: InAtomicMode>(
411        self,
412        _guard: &'rcu A,
413    ) -> PageTableGuard<'rcu, C> where 'a: 'rcu {
414        let guard = PageTableGuard { inner: self };
415
416        proof {
417            guards.guards = guards.guards.insert(owner.slot_vaddr());
418        }
419
420        guard
421    }
422}
423
424impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
425    /// Borrows an entry in the node at a given index.
426    ///
427    /// # Panics
428    ///
429    /// Panics if the index is not within the bound of
430    /// [`nr_subpage_per_huge<C>`].
431    #[verus_spec(res =>
432        with Tracked(owner): Tracked<&NodeOwner<C>>,
433             Tracked(child_owner): Tracked<&EntryOwner<C>>,
434             Tracked(regions): Tracked<&MetaRegionOwners>,
435        requires
436            owner.inv(),
437            child_owner.inv(),
438            owner.relate_guard(*old(self)),
439            child_owner.match_pte(
440                owner.children_perm.value()[idx as int],
441                child_owner.parent_level,
442            ),
443            regions.inv(),
444            regions.contains(owner.slot_index),
445            // Panic condition
446            idx < NR_ENTRIES,
447        ensures
448            res.wf(*child_owner),
449            res.idx == idx,
450            *res.node == *old(self),
451            *final(self) == *final(res.node),
452            owner.relate_guard(*res.node),
453    )]
454    pub fn entry<'a>(&'a mut self, idx: usize) -> Entry<'a, 'rcu, C> {
455        #[cfg(feature = "allow_panic")]
456        assert!(idx < nr_subpage_per_huge::<C>());
457        // SAFETY: The index is within the bound. `Entry::new_at` returns an
458        // entry whose node is the guard value we were handed.
459        unsafe {
460            #[verus_spec(with Tracked(child_owner), Tracked(owner), Tracked(regions))]
461            Entry::new_at(self, idx)
462        }
463    }
464
465    /// Gets the number of valid PTEs in a page table node.
466    /// # Verified Properties
467    /// ## Preconditions
468    /// - The node must be well-formed.
469    /// ## Postconditions
470    /// - Returns the number of valid PTEs in the node.
471    /// ## Safety
472    /// - We require the caller to provide a permission token to ensure that this function is only called on a valid page table node.
473    #[verus_spec(nr =>
474        with Tracked(owner) : Tracked<&NodeOwner<C>>,
475        requires
476            owner.meta_own.nr_children.id() == owner.meta_value().nr_children.id(),
477            self.inner.inner@.invariants(*owner),
478            self.inner.inner@.external_meta_wf(owner.frame_permission.resource(), ()),
479        returns
480            owner.meta_own.nr_children.value(),
481    )]
482    pub fn nr_children(&self) -> u16 {
483        #[verus_spec(with
484            Tracked(Some(owner.tracked_borrow_metadata_perm())),
485            Tracked(&())
486        )]
487        let meta = self.meta();
488
489        *meta.nr_children.borrow(Tracked(&owner.meta_own.nr_children))
490    }
491
492    /// Returns if the page table node is detached from its parent.
493    #[verus_spec(res =>
494        with
495            Tracked(metadata_perms): Tracked<&'a MetadataPerm>,
496            Tracked(repr_perm): Tracked<&'a ()>,
497            Ghost(stray_id): Ghost<vstd::cell::CellId>,
498        requires
499            old(self).inner.inner@.external_meta_wf(*metadata_perms, *repr_perm),
500            typed_meta_value::<PageTablePageMeta<C>>(
501                *metadata_perms,
502                *repr_perm,
503            ).stray.id()
504                == stray_id,
505        ensures
506            res.id() == stray_id,
507            *final(self) == *old(self),
508    )]
509    pub(super) fn stray_mut<'a>(&'a mut self) -> &'a pcell_maybe_uninit::PCell<bool> {
510        // SAFETY: The lock is held so we have an exclusive access.
511        #[verus_spec(with
512            Tracked(Some(metadata_perms)),
513            Tracked(repr_perm)
514        )]
515        let meta = self.meta();
516        &meta.stray
517    }
518
519    /// Reads a non-owning PTE at the given index.
520    ///
521    /// A non-owning PTE means that it does not account for a reference count
522    /// of the a page if the PTE points to a page. The original PTE still owns
523    /// the child page.
524    ///
525    /// # Safety
526    ///
527    /// The caller must ensure that the index is within the bound.
528    #[verus_spec(pte =>
529        with Tracked(owner): Tracked<&NodeOwner<C>>,
530             Tracked(regions): Tracked<&MetaRegionOwners>,
531        requires
532            self.inner.inner@.invariants(*owner),
533            regions.inv(),
534            regions.contains(owner.slot_index),
535            idx < NR_ENTRIES,
536        ensures
537            pte == owner.children_perm.value()[idx as int],
538    )]
539    pub unsafe fn read_pte(&self, idx: usize) -> C::E {
540        // debug_assert!(idx < nr_subpage_per_huge::<C>());
541        let ptr = vstd_extra::array_ptr::ArrayPtr::<C::E, NR_ENTRIES>::from_addr(
542            paddr_to_vaddr(self.start_paddr()),
543        );
544
545        // SAFETY:
546        // - The page table node is alive. The index is inside the bound, so the page table entry is valid.
547        // - All page table entries are aligned and accessed with atomic operations only.
548        unsafe {
549            #[verus_spec(with Tracked(&owner.children_perm))]
550            load_pte(ptr.add(idx), Ordering::Relaxed)
551        }
552    }
553
554    /// Writes a page table entry at a given index.
555    ///
556    /// This operation will leak the old child if the old PTE is present.
557    ///
558    /// # Safety
559    ///
560    /// The caller must ensure that:
561    ///  1. The index must be within the bound;
562    ///  2. The PTE must represent a valid [`Child`] whose level is compatible
563    ///     with the page table node.
564    ///  3. The page table node will have the ownership of the [`Child`]
565    ///     after this method.
566    #[verus_spec(
567        with Tracked(owner): Tracked<&mut NodeOwner<C>>,
568             Tracked(regions): Tracked<&MetaRegionOwners>,
569        requires
570            old(self).inner.inner@.invariants(*old(owner)),
571            regions.inv(),
572            regions.contains(old(owner).slot_index),
573            idx < NR_ENTRIES,
574        ensures
575            final(owner).inv(),
576            final(owner).level() == old(owner).level(),
577            final(owner).meta_own == old(owner).meta_own,
578            final(owner).frame_permission == old(owner).frame_permission,
579            final(owner).slot_index == old(owner).slot_index,
580            final(owner).children_perm.value() == old(owner).children_perm.value().update(
581                idx as int,
582                pte,
583            ),
584            *final(self) == *old(self),
585    )]
586    pub unsafe fn write_pte(&mut self, idx: usize, pte: C::E) {
587        // debug_assert!(idx < nr_subpage_per_huge::<C>());
588        #[verusfmt::skip]
589        let ptr = vstd_extra::array_ptr::ArrayPtr::<C::E, NR_ENTRIES>::from_addr(
590            paddr_to_vaddr(self.start_paddr())
591        );
592
593        // SAFETY:
594        // - The page table node is alive. The index is inside the bound, so the page table entry is valid.
595        // - All page table entries are aligned and accessed with atomic operations only.
596        unsafe {
597            #[verus_spec(with Tracked(&mut owner.children_perm))]
598            store_pte(ptr.add(idx), pte, Ordering::Release)
599        }
600        proof {
601            assert(owner.children_perm.wf());
602        }
603    }
604
605    /// Gets the mutable reference to the number of valid PTEs in the node.
606    #[verus_spec(res =>
607        with
608            Tracked(metadata_perms): Tracked<&'a MetadataPerm>,
609            Ghost(nr_children_id): Ghost<vstd::cell::CellId>,
610        requires
611            old(self).inner.inner@.external_meta_wf(*metadata_perms, ()),
612            typed_meta_value::<PageTablePageMeta<C>>(
613                *metadata_perms,
614                (),
615            ).nr_children.id()
616                == nr_children_id,
617        ensures
618            res.id() == nr_children_id,
619            *final(self) == *old(self),
620    )]
621    fn nr_children_mut<'a>(&'a mut self) -> &'a pcell_maybe_uninit::PCell<u16> {
622        // SAFETY: The lock is held so we have an exclusive access.
623        #[verus_spec(with
624            Tracked(Some(metadata_perms)),
625            Tracked(&())
626        )]
627        let meta = self.meta();
628        &meta.nr_children
629    }
630}
631
632/*impl<C: PageTableConfig> Drop for PageTableGuard<'_, C> {
633    fn drop(&mut self) {
634        self.inner.meta().lock.store(0, Ordering::Release);
635    }
636}*/
637
638impl<C: PageTableConfig> PageTablePageMeta<C> {
639    pub fn new(level: PagingLevel) -> Self {
640        Self {
641            nr_children: pcell_maybe_uninit::PCell::new(0).0,
642            stray: pcell_maybe_uninit::PCell::new(false).0,
643            level,
644            lock: PAtomicU8::new(0).0,
645            _phantom: PhantomData,
646        }
647    }
648
649    /// The PTE value that `read_once::<C::E>` would produce at cursor `c`
650    /// against the given memory view. Linked to `read_once` via
651    /// `pod_bytes(v) == read_view.read_bytes(...)` (strengthened ensures)
652    /// and the checked byte-decoding model.
653    pub open spec fn walk_pte_at_view(view: crate::specs::mm::virt_mem::MemView, c: usize) -> C::E {
654        ostd_pod::decode_pod::<C::E>(view.read_bytes(c, core::mem::size_of::<C::E>()))
655    }
656
657    /// Single-cursor projection of [`walk_coverage_from_view`]. Extracting
658    /// the forall body to a named predicate lets the body invoke
659    /// [`lemma_coverage_at`] for one specific `c` instead of relying on
660    /// auto-trigger matching across the loop invariant's `forall|c|`.
661    pub open spec fn walk_coverage_at(
662        self,
663        view: crate::specs::mm::virt_mem::MemView,
664        dom: vstd::set::Set<int>,
665        c: usize,
666    ) -> bool {
667        let pte = Self::walk_pte_at_view(view, c);
668        pte.is_present() && !pte.is_last(self.level) ==> dom.contains(frame_to_index(pte.paddr()))
669    }
670
671    /// Instantiate [`walk_coverage_from_view`]'s forall at one cursor.
672    pub proof fn lemma_coverage_at(
673        self,
674        reader: crate::mm::VmReader<'_, crate::mm::Infallible>,
675        view: crate::specs::mm::virt_mem::MemView,
676        dom: vstd::set::Set<int>,
677        c: usize,
678    )
679        requires
680            self.walk_coverage_from_view(reader, view, dom),
681            reader.cursor.vaddr <= c,
682            c + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),
683            (c - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,
684        ensures
685            self.walk_coverage_at(view, dom, c),
686    {
687    }
688
689    /// Instantiate [`walk_uniqueness_from_view`]'s forall at one cursor pair.
690    pub proof fn lemma_uniqueness_at_pair(
691        self,
692        reader: crate::mm::VmReader<'_, crate::mm::Infallible>,
693        view: crate::specs::mm::virt_mem::MemView,
694        c1: usize,
695        c2: usize,
696    )
697        requires
698            self.walk_uniqueness_from_view(reader, view),
699            reader.cursor.vaddr <= c1,
700            c1 + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),
701            (c1 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,
702            reader.cursor.vaddr <= c2,
703            c2 + core::mem::size_of::<C::E>() <= reader.cursor.vaddr + reader.remain_spec(),
704            (c2 - reader.cursor.vaddr) % core::mem::size_of::<C::E>() as int == 0,
705            c1 != c2,
706            Self::walk_pte_at_view(view, c1).is_present(),
707            !Self::walk_pte_at_view(view, c1).is_last(self.level),
708            Self::walk_pte_at_view(view, c2).is_present(),
709            !Self::walk_pte_at_view(view, c2).is_last(self.level),
710        ensures
711            Self::walk_pte_at_view(view, c1).paddr() != Self::walk_pte_at_view(view, c2).paddr(),
712    {
713    }
714
715    /// Caller-side dom-membership obligation: every present non-last PTE
716    /// position in the walk (over `view`) has its child-frame index in
717    /// `dom`. Phrased over a frozen `(view, dom)` pair so the body can
718    /// carry it as a loop invariant against an entry-state snapshot
719    /// while `vm_io_owner` advances per iteration.
720    pub open spec fn walk_coverage_from_view(
721        self,
722        reader: crate::mm::VmReader<'_, crate::mm::Infallible>,
723        view: crate::specs::mm::virt_mem::MemView,
724        dom: vstd::set::Set<int>,
725    ) -> bool {
726        forall|c: usize|
727            #![trigger Self::walk_pte_at_view(view, c)]
728            reader.cursor.vaddr <= c && c + core::mem::size_of::<C::E>() <= reader.cursor.vaddr
729                + reader.remain_spec() && (c - reader.cursor.vaddr) % core::mem::size_of::<
730                C::E,
731            >() as int == 0 ==> {
732                let pte = Self::walk_pte_at_view(view, c);
733                pte.is_present() && !pte.is_last(self.level) ==> dom.contains(
734                    frame_to_index(pte.paddr()),
735                )
736            }
737    }
738
739    /// Caller-side uniqueness obligation: distinct cursor positions with
740    /// present non-last PTEs (in `view`) map to distinct paddrs.
741    pub open spec fn walk_uniqueness_from_view(
742        self,
743        reader: crate::mm::VmReader<'_, crate::mm::Infallible>,
744        view: crate::specs::mm::virt_mem::MemView,
745    ) -> bool {
746        forall|c1: usize, c2: usize|
747            #![trigger Self::walk_pte_at_view(view, c1), Self::walk_pte_at_view(view, c2)]
748            reader.cursor.vaddr <= c1 && c1 + core::mem::size_of::<C::E>() <= reader.cursor.vaddr
749                + reader.remain_spec() && (c1 - reader.cursor.vaddr) % core::mem::size_of::<
750                C::E,
751            >() as int == 0 && reader.cursor.vaddr <= c2 && c2 + core::mem::size_of::<C::E>()
752                <= reader.cursor.vaddr + reader.remain_spec() && (c2 - reader.cursor.vaddr)
753                % core::mem::size_of::<C::E>() as int == 0 && c1 != c2 ==> {
754                let pte1 = Self::walk_pte_at_view(view, c1);
755                let pte2 = Self::walk_pte_at_view(view, c2);
756                pte1.is_present() && !pte1.is_last(self.level) && pte2.is_present()
757                    && !pte2.is_last(self.level) ==> pte1.paddr() != pte2.paddr()
758            }
759    }
760
761    /// Caller-side shape obligation: every paddr in `child_perms.dom()`
762    /// has a slot perm matching the shape `from_raw` + `VerifiedDrop::drop`
763    /// expect (init, alignment, refcount within bounds, last-reference
764    /// shape when refcount == 1).
765    pub open spec fn child_perms_embedding(
766        regions: crate::specs::mm::frame::meta_region_owners::MetaRegionOwners,
767        excluded: vstd::set::Set<int>,
768    ) -> bool {
769        forall|paddr: crate::mm::Paddr|
770            #![trigger regions.slot_owner(paddr)]
771            regions.slots.dom().contains(frame_to_index(paddr)) && !excluded.contains(
772                frame_to_index(paddr),
773            ) ==> {
774                let idx = frame_to_index(paddr);
775                let so = regions.slot_owners[idx];
776                &&& <Frame<Self>>::from_raw_requires(regions, paddr)
777                &&& 0 < so.ref_count() <= REF_COUNT_MAX
778                &&& so.storage_perm().is_init()
779                &&& so.ref_count() == 1 ==> {
780                    &&& so.in_list_perm.value() == 0
781                    &&& so.paths_in_pt.is_empty()
782                }
783            }
784    }
785}
786
787} // verus!
ostd/mm/page_table/node/mod.rs

ostd/mm/page_table/node/
mod.rs
