ostd::specs::mm::embedding::kvirt_store

Struct KVmStore

pub struct KVmStore {
    pub regions: MetaRegionOwners,
    pub kernel_pt: PageTableOwner<KernelPtConfig>,
    pub kvirt_areas: Map<KVirtId, Range<Vaddr>>,
}

Expand description

One-step-soundness store for the kernel virtual area API. Holds the shared regions, the single global kernel page table kernel_pt, and the set of allocated kernel virtual areas (each a Range<Vaddr> handle — see the module docs).

The kernel analog of super::VmStore; see the module documentation for how it differs (one global PT vs. a map of user VmSpaces).

Fields§

§regions: MetaRegionOwners§kernel_pt: PageTableOwner<KernelPtConfig>§kvirt_areas: Map<KVirtId, Range<Vaddr>>

Implementations§

Source §

impl KVmStore

Source

pub open spec fn inv(self) -> bool

{
    &&& self.regions.inv()
    &&& self.kernel_pt.inv()
    &&& self.kernel_pt.metaregion_sound(self.regions)
    &&& forall |id: KVirtId| {
        #[trigger] self.kvirt_areas.dom().contains(id)
            ==> {
                let r = self.kvirt_areas[id];
                &&& KERNEL_BASE_VADDR <= r.start
                &&& r.end <= FRAME_METADATA_BASE_VADDR
                &&& r.start % PAGE_SIZE == 0
                &&& r.end % PAGE_SIZE == 0
                &&& r.start <= r.end

            }
    }

}

The store’s top-level invariant.

Mirrors the page-table-soundness portion of super::VmStore::structural_inv (the kernel PT relates to the region map via PageTableOwner::metaregion_sound) and adds the per-area range well-formedness that [KVirtArea::inv] enforces at the handle level (within the kernel VMALLOC bounds, page-aligned, ordered).

Source §

impl KVmStore

Source

pub proof fn step_query<'rcu>(tracked &mut self, id: KVirtId, addr: Vaddr, tracked guards: &mut Guards<'rcu>, root_guard: PageTableGuard<'rcu, KernelPtConfig>, ) -> res : Option<MappedItem>

requires

old(self).inv(),

old(self).kvirt_areas.dom().contains(id),

old(self).kvirt_areas[id].start <= addr < old(self).kvirt_areas[id].end,

!(KVirtArea {
    range: old(self).kvirt_areas[id],
})
    .query_panic_condition(
        KVirtAreaOwner {
            pt_owner: old(self).kernel_pt,
        },
        addr,
        old(self).regions,
    ),

ensures

final(self).inv(),

final(self).kvirt_areas == old(self).kvirt_areas,

({
    let area = KVirtArea {
        range: old(self).kvirt_areas[id],
    };
    let owner = KVirtAreaOwner {
        pt_owner: old(self).kernel_pt,
    };
    &&& area.query_some_condition(owner, addr)
        ==> area.query_some_ensures(owner, addr, res)
    &&& !area.query_some_condition(owner, addr) ==> KVirtArea::query_none_ensures(res)

}),

KVirtArea::query: read the mapped item at the page containing addr in area id. Checks the kernel PT out into a cursor, queries (cloning the resolved leaf — regions refcount bump), and checks it back in, so the store keeps a sound kernel_pt. The caller supplies the ambient lock state (guards / root_guard), as the exec does.