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 vstd::prelude::*;
35use vstd_extra::prelude::Inv;
36
37use crate::specs::{
38    arch::PAGE_SIZE,
39    mm::{
40        frame::meta_region_owners::MetaRegionOwners,
41        page_table::{node::Guards, *},
42    },
43};
44
45use crate::mm::{
46    Vaddr,
47    kspace::{
48        FRAME_METADATA_BASE_VADDR, KERNEL_BASE_VADDR, KernelPtConfig, MappedItem,
49        kvirt_area::{KVirtArea, KVirtAreaOwner},
50    },
51    page_table::PageTableGuard,
52};
53use core::ops::Range;
54
55verus! {
56
57/// Logical identifier for an allocated [`KVirtArea`] in the store.
58pub type KVirtId = int;
59
60/// One-step-soundness store for the kernel virtual area API. Holds the
61/// shared `regions`, the single global kernel page table `kernel_pt`,
62/// and the set of allocated kernel virtual areas (each a `Range<Vaddr>`
63/// handle — see the module docs).
64///
65/// The kernel analog of [`super::VmStore`]; see the module documentation
66/// for how it differs (one global PT vs. a map of user `VmSpace`s).
67pub tracked struct KVmStore {
68    pub regions: MetaRegionOwners,
69    pub kernel_pt: PageTableOwner<KernelPtConfig>,
70    pub kvirt_areas: Map<KVirtId, Range<Vaddr>>,
71}
72
73impl KVmStore {
74    /// The store's top-level invariant.
75    ///
76    /// Mirrors the page-table-soundness portion of
77    /// [`super::VmStore::structural_inv`] (the kernel PT relates to the
78    /// region map via [`PageTableOwner::metaregion_sound`]) and adds the
79    /// per-area range well-formedness that [`KVirtArea::inv`] enforces at
80    /// the handle level (within the kernel VMALLOC bounds, page-aligned,
81    /// ordered).
82    pub open spec fn inv(self) -> bool {
83        &&& self.regions.inv()
84        &&& self.kernel_pt.inv()
85        // The global kernel page table relates to the shared region map —
86        // every present page-table node sits at a sound region slot, just
87        // as `VmStore::inv` requires of each cursor's owner.
88        &&& self.kernel_pt.metaregion_sound(
89            self.regions,
90        )
91        // Each allocated area is a well-formed kernel virtual range:
92        // within `[KERNEL_BASE_VADDR, FRAME_METADATA_BASE_VADDR]` (the
93        // VMALLOC region the real allocator draws from), page-aligned,
94        // and ordered — exactly the handle-level facts `KVirtArea::inv`
95        // guarantees at construction and every op preserves.
96        &&& forall|id: KVirtId| #[trigger]
97            self.kvirt_areas.dom().contains(id) ==> {
98                let r = self.kvirt_areas[id];
99                &&& KERNEL_BASE_VADDR <= r.start
100                &&& r.end <= FRAME_METADATA_BASE_VADDR
101                &&& r.start % PAGE_SIZE == 0
102                &&& r.end % PAGE_SIZE == 0
103                &&& r.start <= r.end
104            }
105    }
106}
107
108} // verus!
ostd/specs/mm/embedding/kvirt_store.rs

ostd/specs/mm/embedding/
kvirt_store.rs
