ostd/specs/mm/embedding/
kvirt_store.rs

1//! Kernel-side one-step-soundness store for the kernel virtual area API
2//! ([`crate::mm::kspace::kvirt_area::KVirtArea`]) — the *kernel* analog of
3//! [`super::VmStore`].
4//!
5//! # Why a separate, kernel store
6//!
7//! [`super::VmStore`] models a caller of the **user** `VmSpace` API: it
8//! holds a `Map<VmSpaceId, VmSpaceOwner>`, each wrapping an
9//! `OwnerSubtree<UserPtConfig>`, plus user-space cursors
10//! (`CursorOwner<'rcu, UserPtConfig>`). `KVirtArea` instead maps frames
11//! into the single, global **kernel** page table
12//! ([`crate::mm::kspace::KERNEL_PAGE_TABLE`], a `KernelPtConfig` table),
13//! so the kernel store differs in three ways:
14//!
15//!   - **one** page table, not a map: a single
16//!     [`PageTableOwner<KernelPtConfig>`] (`kernel_pt`) rather than
17//!     `Map<VmSpaceId, _>`;
18//!   - it tracks the allocated **kernel virtual areas**
19//!     (`kvirt_areas`) — each `KVirtArea` is just a `Range<Vaddr>`
20//!     handle, since its `KVirtAreaOwner` is consumed into the page table
21//!     at construction (`map_frames`/`map_untracked_frames` take it by
22//!     value);
23//!   - cursors and owners are over `KernelPtConfig`, not `UserPtConfig`
24//!     (added when the mutating ops land).
25//!
26//! # Roadmap
27//!
28//! Landed: the store + invariant. Next: `step_query` (read-only) over
29//! `kernel_pt`, then `map_frames` / `map_untracked_frames` (the
30//! mapping-creating ops; their exec ensures may need strengthening
31//! first). Accounting (the `rc == H + P + cover_count` equation
32//! [`super::VmStore`] carries) is deferred — `KVirtArea` is
33//! mapping-focused, not reference-count-focused.
34use core::ops::Range;
35
36use vstd::prelude::*;
37use vstd_extra::prelude::Inv;
38
39use crate::specs::{
40    arch::PAGE_SIZE,
41    mm::{
42        frame::meta_region_owners::MetaRegionOwners,
43        page_table::{node::Guards, *},
44    },
45};
46
47use crate::mm::{
48    Vaddr,
49    kspace::{
50        FRAME_METADATA_BASE_VADDR, KERNEL_BASE_VADDR, KernelPtConfig, MappedItem,
51        kvirt_area::{KVirtArea, KVirtAreaOwner},
52    },
53    page_table::PageTableGuard,
54};
55
56verus! {
57
58/// Logical identifier for an allocated [`KVirtArea`] in the store.
59pub type KVirtId = int;
60
61/// One-step-soundness store for the kernel virtual area API. Holds the
62/// shared `regions`, the single global kernel page table `kernel_pt`,
63/// and the set of allocated kernel virtual areas (each a `Range<Vaddr>`
64/// handle — see the module docs).
65///
66/// The kernel analog of [`super::VmStore`]; see the module documentation
67/// for how it differs (one global PT vs. a map of user `VmSpace`s).
68pub tracked struct KVmStore {
69    pub regions: MetaRegionOwners,
70    pub kernel_pt: PageTableOwner<KernelPtConfig>,
71    pub kvirt_areas: Map<KVirtId, Range<Vaddr>>,
72}
73
74impl KVmStore {
75    /// The store's top-level invariant.
76    ///
77    /// Mirrors the page-table-soundness portion of
78    /// [`super::VmStore::structural_inv`] (the kernel PT relates to the
79    /// region map via [`PageTableOwner::metaregion_sound`]) and adds the
80    /// per-area range well-formedness that [`KVirtArea::inv`] enforces at
81    /// the handle level (within the kernel VMALLOC bounds, page-aligned,
82    /// ordered).
83    pub open spec fn inv(self) -> bool {
84        &&& self.regions.inv()
85        &&& self.kernel_pt.inv()
86        // The global kernel page table relates to the shared region map —
87        // every present page-table node sits at a sound region slot, just
88        // as `VmStore::inv` requires of each cursor's owner.
89        &&& self.kernel_pt.metaregion_sound(
90            self.regions,
91        )
92        // Each allocated area is a well-formed kernel virtual range:
93        // within `[KERNEL_BASE_VADDR, FRAME_METADATA_BASE_VADDR]` (the
94        // VMALLOC region the real allocator draws from), page-aligned,
95        // and ordered — exactly the handle-level facts `KVirtArea::inv`
96        // guarantees at construction and every op preserves.
97        &&& forall|id: KVirtId| #[trigger]
98            self.kvirt_areas.dom().contains(id) ==> {
99                let r = self.kvirt_areas[id];
100                &&& KERNEL_BASE_VADDR <= r.start
101                &&& r.end <= FRAME_METADATA_BASE_VADDR
102                &&& r.start % PAGE_SIZE == 0
103                &&& r.end % PAGE_SIZE == 0
104                &&& r.start <= r.end
105            }
106    }
107}
108
109} // verus!
ostd/specs/mm/embedding/kvirt_store.rs

ostd/specs/mm/embedding/
kvirt_store.rs
