ostd/mm/page_table/node/
entry.rs

1// SPDX-License-Identifier: MPL-2.0
2//! This module provides accessors to the page table entries in a node.
3use vstd::prelude::*;
4
5use vstd::simple_pptr::{self, PPtr, PointsTo};
6
7use vstd_extra::cast_ptr;
8use vstd_extra::drop_tracking::ManuallyDrop;
9use vstd_extra::ghost_tree::*;
10use vstd_extra::ownership::*;
11
12use crate::mm::frame::meta::mapping::{frame_to_index, frame_to_meta, meta_to_frame};
13use crate::mm::frame::{Frame, FrameRef};
14use crate::mm::page_table::*;
15use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
16use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
17use crate::specs::arch::paging_consts::PagingConsts;
18use crate::specs::mm::frame::meta_owners::{MetaSlotOwner, REF_COUNT_UNUSED};
19use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
20use crate::specs::mm::page_table::{PageTableOwner, INC_LEVELS};
21use crate::specs::task::InAtomicMode;
22
23use core::marker::PhantomData;
24use core::ops::Deref;
25
26use crate::{
27    mm::{nr_subpage_per_huge, page_prop::PageProperty},
28    //    sync::RcuDrop,
29    //    task::atomic_mode::InAtomicMode,
30};
31
32use super::*;
33
34verus! {
35
36/// A reference to a page table node.
37pub type PageTableNodeRef<'a, C> = FrameRef<'a, PageTablePageMeta<C>>;
38
39/// A guard that holds the lock of a page table node.
40pub struct PageTableGuard<'rcu, C: PageTableConfig> {
41    pub inner: PageTableNodeRef<'rcu, C>,
42}
43
44impl<'rcu, C: PageTableConfig> Deref for PageTableGuard<'rcu, C> {
45    type Target = PageTableNodeRef<'rcu, C>;
46
47    #[verus_spec(ensures returns self.inner)]
48    fn deref(&self) -> &Self::Target {
49        &self.inner
50    }
51}
52
53pub struct Entry<'rcu, C: PageTableConfig> {
54    /// The page table entry.
55    ///
56    /// We store the page table entry here to optimize the number of reads from
57    /// the node. We cannot hold a `&mut E` reference to the entry because that
58    /// other CPUs may modify the memory location for accessed/dirty bits. Such
59    /// accesses will violate the aliasing rules of Rust and cause undefined
60    /// behaviors.
61    ///
62    /// # Verification Design
63    /// The concrete value of a PTE is specific to the architecture and the page table configuration,
64    /// represented by the type `C::E`. We represent its value as an abstract [`EntryOwner`], which is
65    /// connected to the concrete value by `match_pte`. The `EntryOwner` is well-formed with respect to
66    /// `Entry` if it is related to the concrete value by `match_pte`.
67    ///
68    /// An `Entry` can be thought of as a mutable handle to the concrete value of the PTE.
69    /// The `node` field points (with a level of indirection) to the node that contains the entry,
70    /// `index` provides the offset, and the `pte` is current value. Only one `Entry` can exist for
71    /// a given node at any given time.
72    pub pte: C::E,
73    /// The index of the entry in the node.
74    pub idx: usize,
75    /// The node that contains the entry. In the original Rust this is a `&mut PageTableGuard`; the PPtr
76    /// type is handling the mutable reference because Verus does not yet support storing such a reference
77    /// in a struct.
78    pub node: PPtr<PageTableGuard<'rcu, C>>,
79}
80
81impl<'rcu, C: PageTableConfig> Entry<'rcu, C> {
82    pub open spec fn new_spec(pte: C::E, idx: usize, node: PPtr<PageTableGuard<'rcu, C>>) -> Self {
83        Self { pte, idx, node }
84    }
85
86    #[verifier::when_used_as_spec(new_spec)]
87    pub fn new(pte: C::E, idx: usize, node: PPtr<PageTableGuard<'rcu, C>>) -> Self {
88        Self { pte, idx, node }
89    }
90}
91
92#[verus_verify]
93impl<'a, 'rcu, C: PageTableConfig> Entry<'rcu, C> {
94    /// Returns if the entry does not map to anything.
95    #[verus_spec(r =>
96        with Tracked(owner): Tracked<&EntryOwner<C>>,
97        requires
98            self.wf(*owner),
99            owner.inv(),
100        returns owner.is_absent(),
101    )]
102    pub(in crate::mm) fn is_none(&self) -> bool {
103        !self.pte.is_present()
104    }
105
106    /// Returns if the entry maps to a page table node.
107    #[verus_spec(
108        with Tracked(owner): Tracked<EntryOwner<C>>,
109            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
110            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
111    )]
112    pub(in crate::mm) fn is_node(&self) -> bool
113        requires
114            owner.inv(),
115            self.wf(owner),
116            guard_perm.addr() == self.node.addr(),
117            parent_owner.relate_guard_perm(*guard_perm),
118            parent_owner.inv(),
119            parent_owner.level == owner.parent_level,
120        returns
121            owner.is_node(),
122    {
123        let guard = self.node.borrow(Tracked(guard_perm));
124
125        self.pte.is_present() && !self.pte.is_last(
126            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
127            guard.level(),
128        )
129    }
130
131    /// Gets a reference to the child.
132    #[verus_spec(
133        with Tracked(owner): Tracked<&EntryOwner<C>>,
134            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
135            Tracked(regions): Tracked<&mut MetaRegionOwners>,
136            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
137    )]
138    pub(in crate::mm) fn to_ref(&self) -> (res: ChildRef<'rcu, C>)
139        requires
140            self.invariants(*owner, *old(regions)),
141            self.node_matching(*owner, *parent_owner, *guard_perm),
142            !owner.in_scope,
143        ensures
144            res.invariants(*owner, *regions),
145            regions.slot_owners =~= old(regions).slot_owners,
146            forall |k: usize| old(regions).slots.contains_key(k) ==> #[trigger] regions.slots.contains_key(k),
147            regions.inv(),
148    {
149        let guard = self.node.borrow(Tracked(guard_perm));
150
151        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
152        let level = guard.level();
153
154        // SAFETY:
155        //  - The PTE outlives the reference (since we have `&self`).
156        //  - The level matches the current node.
157        #[verus_spec(with Tracked(regions), Tracked(owner))]
158        let res = ChildRef::from_pte(&self.pte, level);
159
160        res
161    }
162
163    /// Operates on the mapping properties of the entry.
164    ///
165    /// It only modifies the properties if the entry is present.
166    ///
167    /// # Verified Properties
168    /// ## Preconditions
169    /// - **Safety Invariants**: The entry must satisfy the relevant safety invariants.
170    /// - **Safety**: The caller must provide a valid guard permission matching `guard_perm`, and it must be guarding the
171    /// correct parent node.
172    /// - **Safety**: The entry must be a frame.
173    /// ## Postconditions
174    /// - **Safety Invariants**: The entry continues to satisfy the relevant safety invariants.
175    /// - **Safety**: The guard permission is preserved.
176    /// - **Correctness**: The entry's permissions are updated by `op`
177    /// ## Safety
178    /// - The entry is updated in place, only changing its properties, so the metadata is unchanged.
179    /// That's why we don't take a `MetaRegionOwners` argument. It means that all invariants will be preserved.
180    #[verus_spec(
181        with Tracked(owner) : Tracked<&mut EntryOwner<C>>,
182            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
183            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>,
184    )]
185    pub(in crate::mm) fn protect(&mut self, op: impl FnOnce(PageProperty) -> PageProperty)
186        requires
187            old(owner).inv(),
188            old(self).wf(*old(owner)),
189            old(self).node_matching(*old(owner), *old(parent_owner), *old(guard_perm)),
190            op.requires((old(self).pte.prop(),)),
191            old(owner).is_frame(),
192        ensures
193            owner.inv(),
194            self.wf(*owner),
195            self.node_matching(*owner, *parent_owner, *guard_perm),
196            self.parent_perms_preserved(*old(parent_owner), *parent_owner, *old(guard_perm), *guard_perm),
197            owner.is_frame(),
198            owner.frame.unwrap().mapped_pa == old(owner).frame.unwrap().mapped_pa,
199            owner.frame.unwrap().slot_perm == old(owner).frame.unwrap().slot_perm,
200            owner.path == old(owner).path,
201            owner.parent_level == old(owner).parent_level,
202            owner.in_scope == old(owner).in_scope,
203            self.idx == old(self).idx,
204            old(self).pte.is_present() ==> op.ensures((old(owner).frame.unwrap().prop,), owner.frame.unwrap().prop),
205    {
206        let ghost pte0 = self.pte;
207
208        if !self.pte.is_present() {
209            return ;
210        }
211        let prop = self.pte.prop();
212        let new_prop = op(prop);
213
214        /*if prop == new_prop {
215            return;
216        }*/
217
218        proof {
219            self.pte.set_prop_properties(new_prop);
220        }
221        self.pte.set_prop(new_prop);
222
223        let mut guard = self.node.take(Tracked(guard_perm));
224
225        // SAFETY:
226        //  1. The index is within the bounds.
227        //  2. We replace the PTE with a new one, which differs only in
228        //     `PageProperty`, so the level still matches the current
229        //     page table node.
230        #[verus_spec(with Tracked(parent_owner))]
231        guard.write_pte(self.idx, self.pte);
232
233        proof {
234            let tracked mut frame_owner = owner.frame.tracked_take();
235            frame_owner.prop = new_prop;
236            owner.frame = Some(frame_owner);
237        }
238        assert(owner.match_pte(self.pte, owner.parent_level));
239
240        self.node.put(Tracked(guard_perm), guard);
241    }
242
243    /// Replaces the entry with a new child.
244    ///
245    /// The old child is returned.
246    ///
247    /// # Verified Properties
248    /// ## Preconditions
249    /// - **Safety Invariants**: Both old and new owners must satisfy the respective safety invariants for an [Entry](Entry::invariants)
250    /// and a [Child](Child::invariants).
251    /// - **Safety**: The caller must provide valid owners for all objects, and for the parent node where the entry
252    /// is being replaced. The parent node must have a valid guard permission.
253    /// - **Correctness**: The new child must be compatible with the old, for instance by having the same level.
254    /// ## Postconditions
255    /// - **Safety Invariants**: The old and new owners will satisfy the safety invariants for an [Entry](Entry::invariants)
256    /// and a [Child](Child::invariants), but they have changed positions.
257    /// - **Safety**: Safety properties that hold across the page table's tree structure are preserved
258    /// everywhere except for the entry being replaced.
259    /// - **Correctness**: The entry will match the argument, and the returned child will match the entry that was replaced.
260    /// ## Safety
261    /// - The invariants ensure that the entry is appropriately aligned and its index is within bounds.
262    /// - The transformation from child to entry ensures that the tree now owns the updated entry.
263    #[verus_spec(
264        with Tracked(regions) : Tracked<&mut MetaRegionOwners>,
265            Tracked(owner): Tracked<&mut EntryOwner<C>>,
266            Tracked(new_owner): Tracked<&mut EntryOwner<C>>,
267            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
268            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>
269    )]
270    pub(in crate::mm) fn replace(&mut self, new_child: Child<C>) -> (res: Child<C>)
271        requires
272            old(self).invariants(*old(owner), *old(regions)),
273            new_child.invariants(*old(new_owner), *old(regions)),
274            old(self).node_matching(*old(owner), *old(parent_owner), *old(guard_perm)),
275            old(self).new_owner_compatible(new_child, *old(owner), *old(new_owner), *old(regions)),
276            !old(owner).in_scope,
277            Self::replace_panic_condition(*old(parent_owner), *old(new_owner)),
278        ensures
279            self.invariants(*new_owner, *regions),
280            res.invariants(*owner, *regions),
281            self.node_matching(*new_owner, *parent_owner, *guard_perm),
282            self.idx == old(self).idx,
283            *owner == old(owner).from_pte_owner_spec(),
284            *new_owner == old(new_owner).into_pte_owner_spec(),
285            Self::relate_region_neq_preserved(*old(owner), *new_owner, *old(regions), *regions),
286            Self::path_tracked_pred_preserved(*old(regions), *regions),
287            !new_owner.is_absent() ==> PageTableOwner::<C>::path_tracked_pred(*regions)(*new_owner, new_owner.path),
288            self.parent_perms_preserved(*old(parent_owner), *parent_owner, *guard_perm, *old(guard_perm)),
289            // path_if_in_pt only changes for the new owner's slot; all other slots preserve their value.
290            forall|idx: usize| #![trigger regions.slot_owners[idx].path_if_in_pt]
291                (new_owner.is_absent() || idx != frame_to_index(new_owner.meta_slot_paddr().unwrap()))
292                    ==> regions.slot_owners[idx].path_if_in_pt == old(regions).slot_owners[idx].path_if_in_pt,
293    {
294        let ghost new_idx = frame_to_index(new_owner.meta_slot_paddr().unwrap());
295        let ghost old_idx = frame_to_index(owner.meta_slot_paddr().unwrap());
296
297        let mut guard = self.node.take(Tracked(guard_perm));
298
299        /*
300        match &new_child {
301            Child::PageTable(node) => {
302                assert(node.level() == guard.level() - 1);
303            }
304            Child::Frame(_, level, _) => {
305                assert(*level == guard.level());
306            }
307            Child::None => {}
308        }
309        */
310
311        // SAFETY:
312        //  - The PTE is not referenced by other `ChildRef`s (since we have `&mut self`).
313        //  - The level matches the current node.
314        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
315        let level = guard.level();
316
317        #[verus_spec(with Tracked(regions), Tracked(owner))]
318        let old_child = Child::from_pte(self.pte, level);
319
320        let ghost regions_after_from = *regions;
321
322        assert(new_owner.is_node() ==> regions.slots.contains_key(frame_to_index(new_owner.meta_slot_paddr().unwrap())));
323
324        if old_child.is_none() && !new_child.is_none() {
325            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
326            let nr_children = guard.nr_children_mut();
327            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
328            assume(_tmp < NR_ENTRIES);
329            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
330        } else if !old_child.is_none() && new_child.is_none() {
331            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
332            let nr_children = guard.nr_children_mut();
333            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
334            assume(_tmp > 0);
335            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp - 1);
336        }
337        proof {
338            assert(owner.relate_region(*regions));
339        }
340
341        #[verus_spec(with Tracked(new_owner), Tracked(regions))]
342        let new_pte = new_child.into_pte();
343
344        let ghost regions_after_into = *regions;
345
346        proof {
347            assert(owner.relate_region(*regions));
348        }
349
350        // SAFETY:
351        //  1. The index is within the bounds.
352        //  2. The new PTE is a valid child whose level matches the current page table node.
353        //  3. The ownership of the child is passed to the page table node.
354        #[verus_spec(with Tracked(parent_owner))]
355        guard.write_pte(self.idx, new_pte);
356
357        self.node.put(Tracked(guard_perm), guard);
358
359        self.pte = new_pte;
360
361        proof {
362            if new_owner.is_node() || new_owner.is_frame() {
363                let paddr = new_owner.meta_slot_paddr().unwrap();
364                regions.inv_implies_correct_addr(paddr);
365
366                let tracked mut new_meta_slot = regions.slot_owners.tracked_remove(new_idx);
367                new_meta_slot.path_if_in_pt = Some(new_owner.get_path());
368                regions.slot_owners.tracked_insert(new_idx, new_meta_slot);
369            }
370            owner.in_scope = true;
371        }
372
373        assert(Self::relate_region_neq_preserved(*old(owner), *new_owner, *old(regions), *regions));
374        assert(Self::path_tracked_pred_preserved(*old(regions), *regions));
375
376        proof {
377            if new_owner.is_node() || new_owner.is_frame() {
378                let paddr = new_owner.meta_slot_paddr().unwrap();
379                regions.inv_implies_correct_addr(paddr);
380            }
381        }
382
383        old_child
384    }
385
386    /// Allocates a new child page table node and replaces the entry with it.
387    ///
388    /// If the old entry is not none, the operation will fail and return `None`.
389    /// Otherwise, the lock guard of the new child page table node is returned.
390    /// # Verified Properties
391    /// ## Preconditions
392    /// - **Safety Invariants**: The old node's root must satisfy the safety invariants for an [Entry](Entry::invariants)
393    /// and the caller must provide its parent node owner.
394    /// ## Postconditions
395    /// - **Safety Invariants**: If a new node is allocated, it will satisfy the safety invariants.
396    /// - **Safety**: If a new node is allocated, all other nodes have their invariants preserved.
397    /// - **Correctness**: A new node is allocated if and only if the old node is absent.
398    /// - **Correctness**: If the old node is present, the function retuns `None` and the state is unchanged.
399    /// ## Safety
400    /// - The invariants ensure that the entry is appropriately aligned and its index is within bounds.
401    /// - The invariants of the entire page table are preserved in both cases.
402    #[verus_spec(res =>
403        with Tracked(owner): Tracked<&mut OwnerSubtree<C>>,
404            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
405            Tracked(regions): Tracked<&mut MetaRegionOwners>,
406            Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
407            Tracked(parent_guard_perm): Tracked<&mut GuardPerm<'rcu, C>>
408            -> guard_perm: Tracked<Option<GuardPerm<'rcu, C>>>
409        requires
410            old(self).invariants(old(owner).value, *old(regions)),
411            old(owner).inv(),
412            old(self).node_matching(old(owner).value, *old(parent_owner), *old(parent_guard_perm)),
413            old(owner).level < INC_LEVELS - 1,
414        ensures
415            self.invariants(owner.value, *regions),
416            self.parent_perms_preserved(*old(parent_owner), *parent_owner, *old(parent_guard_perm), *parent_guard_perm),
417            self.idx == old(self).idx,
418            old(owner).value.is_absent() && old(parent_owner).level > 1 ==> {
419                // node_matching preserved: parent_owner still matches the child after allocation.
420                &&& self.node_matching(owner.value, *parent_owner, *parent_guard_perm)
421                // OwnerSubtree inv (recursive tree invariant, not just value.inv()).
422                &&& owner.inv()
423                // After into_pte, the entry has in_scope == false.
424                &&& !owner.value.in_scope
425            },
426            old(owner).value.is_absent() && old(parent_owner).level > 1 ==> {
427                &&& res is Some
428                &&& owner.value.is_node()
429                &&& guard_perm@ is Some
430                &&& guard_perm@.unwrap().addr() == res.unwrap().addr()
431                &&& owner.level == old(owner).level
432                &&& owner.value.parent_level == old(owner).value.parent_level
433                &&& owner.value.node.unwrap().relate_guard_perm(guard_perm@.unwrap())
434                &&& guards.lock_held(owner.value.node.unwrap().meta_perm.addr())
435                &&& owner.value.path == old(owner).value.path
436                &&& owner.value.relate_region(*regions)
437                &&& OwnerSubtree::implies(
438                    CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
439                    CursorOwner::<'rcu, C>::node_unlocked_except(*guards, owner.value.node.unwrap().meta_perm.addr()))
440                &&& Self::relate_region_neq_preserved(old(owner).value, owner.value, *old(regions), *regions)
441                &&& Self::path_tracked_pred_preserved(*old(regions), *regions)
442                &&& old(regions).slots.contains_key(frame_to_index(owner.value.meta_slot_paddr().unwrap()))
443                &&& owner.tree_predicate_map(owner.value.path,
444                    CursorOwner::<'rcu, C>::node_unlocked_except(*guards, owner.value.node.unwrap().meta_perm.addr()))
445                &&& owner.tree_predicate_map(owner.value.path, PageTableOwner::<C>::relate_region_pred(*regions))
446                &&& owner.tree_predicate_map(owner.value.path, PageTableOwner::<C>::path_tracked_pred(*regions))
447                &&& PageTableOwner(*owner).view_rec(owner.value.path) =~= set![]
448                // All children of the newly allocated node are absent (empty PT node).
449                &&& forall|i: int| 0 <= i < NR_ENTRIES ==>
450                    #[trigger] owner.children[i] is Some && owner.children[i].unwrap().value.is_absent()
451                // slot_owners unchanged for all indices except the new PT node's index.
452                &&& forall|i: usize| i != frame_to_index(owner.value.meta_slot_paddr().unwrap()) ==>
453                    (#[trigger] regions.slot_owners[i]) == old(regions).slot_owners[i]
454                // slots keys: the new PT node was removed then re-inserted, so all old keys preserved.
455                &&& forall|i: usize| old(regions).slots.contains_key(i)
456                    ==> (#[trigger] regions.slots.contains_key(i))
457                // The new PT node's ref_count is not UNUSED (was set to 1 by get_from_unused).
458                &&& regions.slot_owners[frame_to_index(owner.value.meta_slot_paddr().unwrap())]
459                    .inner_perms.ref_count.value() != REF_COUNT_UNUSED
460                // The allocated slot had ref_count == UNUSED before allocation (from get_from_unused).
461                &&& old(regions).slot_owners[frame_to_index(owner.value.meta_slot_paddr().unwrap())]
462                    .inner_perms.ref_count.value() == REF_COUNT_UNUSED
463            },
464            !old(owner).value.is_absent() ==> {
465                &&& res is None
466                &&& *owner == *old(owner)
467            },
468            forall |i: usize| old(guards).lock_held(i) ==> guards.lock_held(i),
469            forall |i: usize| old(guards).unlocked(i) && i != owner.value.node.unwrap().meta_perm.addr() ==> guards.unlocked(i),
470    )]
471    pub(in crate::mm) fn alloc_if_none<A: InAtomicMode>(&mut self, guard: &'rcu A)
472    -> (res: Option<PPtr<PageTableGuard<'rcu, C>>>) {
473        let entry_is_present = self.pte.is_present();
474
475        let mut parent_guard = self.node.take(Tracked(parent_guard_perm));
476
477        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
478        let level = parent_guard.level();
479
480        if entry_is_present || level <= 1 {
481            self.node.put(Tracked(parent_guard_perm), parent_guard);
482
483            proof_with!{|= Tracked(None)}
484            None
485        } else {
486            let tracked old_path = owner.value.get_path();
487
488            proof_decl! {
489                let tracked mut new_node_owner: Tracked<OwnerSubtree<C>>;
490            }
491
492            #[verus_spec(with Tracked(parent_owner), Tracked(regions), Tracked(guards), Ghost(self.idx) => Tracked(new_node_owner))]
493            let new_page = PageTableNode::<C>::alloc(level - 1);
494
495            proof {
496                let pte = C::E::new_pt_spec(meta_to_frame(new_node_owner.value.node.unwrap().meta_perm.addr()));
497                old(parent_owner).set_children_perm_axiom(self.idx, pte);
498                C::E::new_properties();
499                assert(!pte.is_last_spec(level as PagingLevel));
500            }
501
502            #[verus_spec(with Tracked(&new_node_owner.value.node.tracked_borrow().meta_perm.points_to))]
503            let paddr = new_page.start_paddr();
504
505            assert(new_node_owner.value.relate_region(*regions));
506
507            #[verus_spec(with Tracked(&mut new_node_owner.value), Tracked(regions))]
508            let new_pte = Child::PageTable(new_page).into_pte();
509            self.pte = new_pte;
510
511            proof {
512                // Preserve into_pte postcondition before we mutate owner
513                assert(new_node_owner.value.pte_invariants(self.pte, *regions));
514                assert(new_node_owner.value.match_pte(self.pte, new_node_owner.value.parent_level));
515                broadcast use crate::mm::frame::meta::mapping::group_page_meta;
516            }
517
518            #[verus_spec(with Tracked(regions), Tracked(&new_node_owner.value.node.tracked_borrow().meta_perm))]
519            let pt_ref = PageTableNodeRef::borrow_paddr(paddr);
520
521            proof_decl! {
522                let tracked mut guard_perm: Tracked<GuardPerm<'rcu, C>>;
523            }
524
525            // Lock before writing the PTE, so no one else can operate on it.
526            #[verus_spec(with Tracked(&new_node_owner.value.node.tracked_borrow()), Tracked(guards) => Tracked(guard_perm))]
527            let pt_lock_guard = pt_ref.lock(guard);
528
529            // SAFETY:
530            //  1. The index is within the bounds.
531            //  2. The new PTE is a child in `C` and at the correct paging level.
532            //  3. The ownership of the child is passed to the page table node.
533            #[verus_spec(with Tracked(parent_owner))]
534            parent_guard.write_pte(self.idx, self.pte);
535
536            #[verus_spec(with Tracked(&parent_owner.meta_perm))]
537            let nr_children = parent_guard.nr_children_mut();
538            let _tmp = nr_children.read(Tracked(&parent_owner.meta_own.nr_children));
539            assume(_tmp < NR_ENTRIES);
540            nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
541
542            self.node.put(Tracked(parent_guard_perm), parent_guard);
543
544            proof {
545                owner.value = new_node_owner.value;
546                owner.value.parent_level = level as PagingLevel;
547                owner.value.path = old_path;
548                owner.children = new_node_owner.children;
549                // From allocated_empty_node_owner: all children are absent.
550                assert(forall|i: int| 0 <= i < NR_ENTRIES ==>
551                    (#[trigger] owner.children[i]) is Some && owner.children[i].unwrap().value.is_absent());
552
553                let new_paddr = owner.value.meta_slot_paddr().unwrap();
554                assert(old(regions).slots.contains_key(frame_to_index(new_paddr)));
555                regions.inv_implies_correct_addr(new_paddr);
556                let new_idx = frame_to_index(new_paddr);
557                let tracked mut new_meta_slot = regions.slot_owners.tracked_remove(new_idx);
558                new_meta_slot.path_if_in_pt = Some(owner.value.get_path());
559                regions.slot_owners.tracked_insert(new_idx, new_meta_slot);
560            }
561
562            proof_with!{|= Tracked(Some(guard_perm))}
563            Some(pt_lock_guard)
564        }
565    }
566
567    /// Splits the entry to smaller pages if it maps to a huge page.
568    ///
569    /// If the entry does map to a huge page, it is split into smaller pages
570    /// mapped by a child page table node. The new child page table node
571    /// is returned.
572    ///
573    /// If the entry does not map to a untracked huge page, the method returns
574    /// `None`.
575    /// # Verified Properties
576    /// ## Preconditions
577    /// - **Safety Invariants**: The old node's root must satisfy the safety invariants for an [Entry](Entry::invariants)
578    /// and the caller must provide its parent node owner.
579    /// ## Postconditions
580    /// - **Safety Invariants**: The node allocated in place of the split page satisfies the safety invariants.
581    /// - **Safety**: All other nodes have their invariants preserved.
582    #[verus_spec(res =>
583        with Tracked(owner) : Tracked<&mut OwnerSubtree<C>>,
584            Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
585            Tracked(regions): Tracked<&mut MetaRegionOwners>,
586            Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
587            Tracked(guard_perm): Tracked<&mut GuardPerm<'rcu, C>>
588        requires
589            old(regions).inv(),
590            old(owner).inv(),
591            old(self).wf(old(owner).value),
592            old(self).node.addr() == old(guard_perm).addr(),
593            old(guard_perm).is_init(),
594            old(parent_owner).relate_guard_perm(*old(guard_perm)),
595            old(parent_owner).inv(),
596            old(parent_owner).level == old(owner).value.parent_level,
597            old(parent_owner).level < NR_LEVELS,
598        ensures
599            old(owner).value.is_frame() && old(parent_owner).level > 1 ==> {
600                &&& res is Some
601                &&& owner.value.is_node()
602                &&& owner.level == old(owner).level
603                &&& parent_owner.relate_guard_perm(*guard_perm)
604                &&& guards.guards.contains_key(res.unwrap().addr())
605                &&& guards.guards[res.unwrap().addr()] is Some
606                &&& guards.guards[res.unwrap().addr()].unwrap().pptr() == res.unwrap()
607                &&& owner.value.node.unwrap().relate_guard_perm(guards.guards[res.unwrap().addr()].unwrap())
608                &&& owner.value.node.unwrap().meta_perm.addr() == res.unwrap().addr()
609                // All children of the new node subtree are frames with the same prop (from the split loop).
610                &&& forall |j: int| 0 <= j < NR_ENTRIES ==>
611                    (#[trigger] owner.children[j]).unwrap().value.is_frame()
612                &&& forall |j: int| 0 <= j < NR_ENTRIES ==>
613                    (#[trigger] owner.children[j]).unwrap().value.frame.unwrap().prop
614                        == old(owner).value.frame.unwrap().prop
615                &&& owner.value.path == old(owner).value.path
616                &&& owner.value.relate_region(*regions)
617                &&& OwnerSubtree::implies(
618                    CursorOwner::<'rcu, C>::node_unlocked(*old(guards)),
619                    CursorOwner::<'rcu, C>::node_unlocked(*guards))
620                &&& OwnerSubtree::implies(
621                    PageTableOwner::<C>::relate_region_pred(*old(regions)),
622                    PageTableOwner::<C>::relate_region_pred(*regions))
623                &&& owner.tree_predicate_map(owner.value.path,
624                    CursorOwner::<'rcu, C>::node_unlocked(*guards))
625                &&& owner.tree_predicate_map(owner.value.path,
626                    PageTableOwner::<C>::relate_region_pred(*regions))
627            },
628            !old(owner).value.is_frame() || old(parent_owner).level <= 1 ==> {
629                &&& res is None
630                &&& *owner == *old(owner)
631            },
632            owner.inv(),
633            owner.value.parent_level == old(owner).value.parent_level,
634            self.idx == old(self).idx,
635            old(owner).value.is_frame() && old(parent_owner).level > 1 ==> !owner.value.in_scope,
636            old(owner).value.is_frame() && old(parent_owner).level > 1 ==>
637                self.node_matching(owner.value, *parent_owner, *guard_perm),
638            regions.inv(),
639            parent_owner.inv(),
640            parent_owner.level == old(parent_owner).level,
641            guard_perm.pptr() == old(guard_perm).pptr(),
642            guard_perm.value().inner.inner@.ptr.addr() == old(guard_perm).value().inner.inner@.ptr.addr(),
643            forall |i: usize| old(guards).lock_held(i) ==> guards.lock_held(i),
644            forall |i: usize| old(guards).unlocked(i) ==> guards.unlocked(i),
645            // slot_owners unchanged for all indices except the new PT node's index.
646            old(owner).value.is_frame() && old(parent_owner).level > 1 ==> {
647                &&& forall|i: usize| i != frame_to_index(meta_to_frame(owner.value.node.unwrap().meta_perm.addr())) ==>
648                    (#[trigger] regions.slot_owners[i]) == old(regions).slot_owners[i]
649                // slots keys preserved (alloc removes then borrow re-inserts).
650                &&& forall|i: usize| old(regions).slots.contains_key(i)
651                    ==> (#[trigger] regions.slots.contains_key(i))
652                // The new PT node's ref_count is not UNUSED.
653                &&& regions.slot_owners[frame_to_index(meta_to_frame(owner.value.node.unwrap().meta_perm.addr()))]
654                    .inner_perms.ref_count.value() != REF_COUNT_UNUSED
655                // The allocated slot had ref_count == UNUSED before allocation.
656                &&& old(regions).slot_owners[frame_to_index(meta_to_frame(owner.value.node.unwrap().meta_perm.addr()))]
657                    .inner_perms.ref_count.value() == REF_COUNT_UNUSED
658            },
659    )]
660    pub(in crate::mm) fn split_if_mapped_huge<A: InAtomicMode>(&mut self, guard: &'rcu A)
661        -> (res: Option<PPtr<PageTableGuard<'rcu, C>>>) {
662        let mut node_guard = self.node.take(Tracked(guard_perm));
663
664        #[verus_spec(with Tracked(&parent_owner.meta_perm))]
665        let level = node_guard.level();
666
667        if !(self.pte.is_last(level) && level > 1) {
668            self.node.put(Tracked(guard_perm), node_guard);
669
670            return None;
671        }
672        let pa = self.pte.paddr();
673        let prop = self.pte.prop();
674
675        proof {
676            EntryOwner::last_pte_implies_frame_match(owner.value, self.pte, level);
677        }
678
679        proof_decl!{
680            let tracked mut new_owner: OwnerSubtree<C>;
681        }
682
683        #[verus_spec(with Tracked(parent_owner), Tracked(regions), Tracked(guards), Ghost(self.idx) => Tracked(new_owner))]
684        let new_page = PageTableNode::<C>::alloc(level);
685
686        #[verus_spec(with Tracked(&new_owner.value.node.tracked_borrow().meta_perm.points_to))]
687        let paddr = new_page.start_paddr();
688
689        proof {
690            broadcast use crate::mm::frame::meta::mapping::group_page_meta;
691        }
692
693        #[verus_spec(with Tracked(regions), Tracked(&new_owner.value.node.tracked_borrow().meta_perm))]
694        let pt_ref = PageTableNodeRef::borrow_paddr(paddr);
695
696        proof_decl! {
697            let tracked mut new_guard_perm: Tracked<GuardPerm<'rcu, C>>;
698        }
699
700        // Lock before writing the PTE, so no one else can operate on it.
701        #[verus_spec(with Tracked(&new_owner.value.node.tracked_borrow()), Tracked(guards) => Tracked(new_guard_perm))]
702        let pt_lock_guard = pt_ref.lock(guard);
703
704        let ghost children_perm = new_owner.value.node.unwrap().children_perm;
705        let ghost new_owner_path = new_owner.value.path;
706        let ghost new_owner_meta_addr = new_owner.value.node.unwrap().meta_perm.addr();
707
708        for i in 0..nr_subpage_per_huge::<C>()
709            invariant
710                1 < level < NR_LEVELS,
711                owner.inv(),
712                owner.value.is_frame(),
713                owner.value.parent_level == level,
714                owner.value.frame.unwrap().mapped_pa == pa,
715                owner.value.frame.unwrap().prop == prop,
716                pa % page_size(level) == 0,
717                pa + page_size(level) <= MAX_PADDR,
718                regions.inv(),
719                parent_owner.inv(),
720                new_owner.value.is_node(),
721                new_owner.inv(),
722                new_owner.value.path == new_owner_path,
723                new_owner.value.node.unwrap().meta_perm.addr() == new_owner_meta_addr,
724                new_owner.value.node.unwrap().relate_guard_perm(new_guard_perm),
725                new_owner.value.node.unwrap().level == (level - 1) as PagingLevel,
726                pt_lock_guard.addr() == new_guard_perm.addr(),
727                forall|j: int|
728                    #![auto]
729                    0 <= j < NR_ENTRIES ==> {
730                        &&& new_owner.children[j] is Some
731                        &&& new_owner.children[j].unwrap().value.match_pte(new_owner.value.node.unwrap().children_perm.value()[j], new_owner.value.node.unwrap().level)
732                        &&& new_owner.children[j].unwrap().value.parent_level == new_owner.value.node.unwrap().level
733                        &&& new_owner.children[j].unwrap().value.inv()
734                        &&& new_owner.children[j].unwrap().value.path == new_owner_path.push_tail(j as usize)
735                    },
736                forall|j: int| #![auto] i <= j < NR_ENTRIES ==> {
737                    &&& new_owner.children[j].unwrap().value.is_absent()
738                    &&& !new_owner.children[j].unwrap().value.in_scope
739                    &&& new_owner.value.node.unwrap().children_perm.value()[j] == C::E::new_absent_spec()
740                },
741                // Children [0, i) have been replaced with frames.
742                forall|j: int| #![auto] 0 <= j < i ==> {
743                    new_owner.children[j].unwrap().value.is_frame()
744                },
745                new_page.ptr.addr() == new_owner_meta_addr,
746        {
747            proof {
748                C::axiom_nr_subpage_per_huge_eq_nr_entries();
749            }
750            assert(i < NR_ENTRIES);
751
752            proof {
753                // Prove required facts while we still have new_owner.value.node available.
754                let ghost the_node = new_owner.value.node.unwrap();
755                assert(0 <= i < NR_ENTRIES);
756                assert(new_owner.children[i as int].unwrap().value.match_pte(
757                    the_node.children_perm.value()[i as int],
758                    new_owner.children[i as int].unwrap().value.parent_level,
759                ));
760                assert(the_node.relate_guard_perm(new_guard_perm));
761                assert(new_guard_perm.addr() == pt_lock_guard.addr());
762                assert(new_owner.children[i as int].unwrap().value.parent_level == the_node.level);
763                assert(!new_owner.children[i as int].unwrap().value.in_scope);
764
765                OwnerSubtree::child_some_properties(new_owner, i as usize);
766            }
767
768            let tracked mut new_owner_node = new_owner.value.node.tracked_take();
769
770            proof {
771                let ghost old_children_perm = new_owner_node.children_perm;
772            }
773
774            proof {
775                EntryOwner::huge_frame_split_child_at(owner.value, *regions, i as usize);
776            }
777
778            let small_pa = pa + i * page_size(level - 1);
779
780            assert(small_pa % PAGE_SIZE == 0);
781
782            let tracked split_slot_perm = EntryOwner::<C>::placeholder_slot_perm(small_pa, regions);
783            let tracked child_owner = EntryOwner::new_frame(
784                small_pa,
785                new_owner.value.path.push_tail(i as usize),
786                (level - 1) as PagingLevel,
787                prop,
788                split_slot_perm,
789            );
790
791            #[verus_spec(with Tracked(&new_owner_node), Tracked(&new_owner.children.tracked_borrow(i as int).tracked_borrow().value), Tracked(&new_guard_perm))]
792            let mut entry = PageTableGuard::entry(pt_lock_guard, i);
793
794            proof {
795                assert(entry.idx == i as usize);
796                let ghost child_before_remove = new_owner.child(i as usize).unwrap();
797                assert(child_before_remove.inv());
798            }
799            let tracked mut new_owner_child = new_owner.children.tracked_remove(i as int).tracked_unwrap();
800
801            proof {
802                assert(new_owner_child.value.match_pte(
803                    new_owner_node.children_perm.value()[i as int],
804                    new_owner_child.value.parent_level,
805                ));
806
807                let idx = frame_to_index(small_pa);
808                assert(regions.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED);
809                assert(regions.slot_owners[idx].path_if_in_pt is None);
810
811                assert(entry.node_matching(new_owner_child.value, new_owner_node, new_guard_perm)) by {
812                    let pte = new_owner_node.children_perm.value()[i as int];
813                    assert(pte == C::E::new_absent_spec());
814                    crate::specs::arch::PageTableEntry::absent_pte_paddr_ok();
815                    EntryOwner::absent_match_pte(
816                        new_owner_child.value,
817                        pte,
818                        new_owner_child.value.parent_level,
819                    );
820                };
821
822                assert(Child::<C>::Frame(small_pa, (level - 1) as PagingLevel, prop)
823                    .invariants(child_owner, *regions));
824            }
825
826            #[verus_spec(with Tracked(regions),
827                Tracked(&mut new_owner_child.value),
828                Tracked(&mut child_owner),
829                Tracked(&mut new_owner_node),
830                Tracked(&mut new_guard_perm))]
831            let old = entry.replace(Child::Frame(small_pa, level - 1, prop));
832
833            proof {
834                new_owner.value.node = Some(new_owner_node);
835                new_owner_child.value.in_scope = false;
836                child_owner.in_scope = false;
837                OwnerSubtree::set_value_property(new_owner_child, child_owner);
838                new_owner_child.value = child_owner;
839                new_owner.children.tracked_insert(i as int, Some(new_owner_child));
840
841                TreePath::push_tail_property_len(new_owner_path, i as usize);
842                OwnerSubtree::insert_preserves_inv(new_owner, i as usize, new_owner_child);
843            }
844        }
845
846        self.pte = (#[verus_spec(with Tracked(&mut new_owner.value), Tracked(regions))]
847        Child::PageTable(new_page).into_pte());
848
849        proof {
850            new_owner.level = owner.level;
851            *owner = new_owner;
852        }
853
854        let tracked mut node_owner = owner.value.node.tracked_take();
855
856        // SAFETY:
857        //  1. The index is within the bounds.
858        //  2. The new PTE is a child in `C` and at the correct paging level.
859        //  3. The ownership of the child is passed to the page table node.
860        #[verus_spec(with Tracked(&mut node_owner))]
861        node_guard.write_pte(self.idx, self.pte);
862
863        proof {
864            owner.value.node = Some(node_owner);
865        }
866
867        self.node.put(Tracked(guard_perm), node_guard);
868
869        Some(pt_lock_guard)
870    }
871
872    /// Create a new entry at the node with guard.
873    ///
874    /// # Verified Properties
875    /// ## Preconditions
876    /// - **Safety**: The caller must provide the owner of the entry and the parent node, and the entry
877    /// must match the parent node's PTE at the given index.
878    /// - **Safety**: The caller must provide a valid guard permission matching `guard`, and it must be guarding the
879    /// correct parent.
880    /// ## Postconditions
881    /// - **Correctness**: The resulting entry matches the owner.
882    /// ## Safety
883    /// - The precondition ensures that the index is within the bounds of the node.
884    /// - This function does not modify the actual entry or any other relevant structure, so it is safe to call.
885    /// Because we also require the guard to be correct, it will be safe to use the resulting `Entry` as a handle to the
886    /// underlying `PTE`.
887    #[verus_spec(
888        with Tracked(owner): Tracked<&EntryOwner<C>>,
889            Tracked(parent_owner): Tracked<&NodeOwner<C>>,
890            Tracked(guard_perm): Tracked<&GuardPerm<'rcu, C>>
891    )]
892    pub(in crate::mm) fn new_at(guard: PPtr<PageTableGuard<'rcu, C>>, idx: usize) -> (res: Self)
893        requires
894            owner.inv(),
895            !owner.in_scope,
896            parent_owner.inv(),
897            guard_perm.addr() == guard.addr(),
898            parent_owner.relate_guard_perm(*guard_perm),
899            idx < NR_ENTRIES,
900            owner.match_pte(parent_owner.children_perm.value()[idx as int], owner.parent_level),
901        ensures
902            res.wf(*owner),
903            res.node.addr() == guard_perm.addr(),
904            res.idx == idx,
905    {
906        // SAFETY: The index is within the bound.
907        let guard_val = guard.borrow(Tracked(guard_perm));
908        #[verus_spec(with Tracked(parent_owner))]
909        let pte = guard_val.read_pte(idx);
910        Self { pte, idx, node: guard }
911    }
912}
913
914} // verus!
ostd/mm/page_table/node/entry.rs

ostd/mm/page_table/node/
entry.rs
