Skip to main content

KVmStore

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§

impl KVmStore

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).

Auto Trait Implementations§

impl Freeze for KVmStore

impl !RefUnwindSafe for KVmStore

impl Send for KVmStore

impl Sync for KVmStore

impl Unpin for KVmStore

impl UnsafeUnpin for KVmStore

impl UnwindSafe for KVmStore

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

impl<A> SpecEq<&A> for A
where A: ?Sized,

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

impl<A> SpecEq<A> for A
where A: ?Sized,

impl<A> SpecEq<Ghost<A>> for A

impl<A> SpecEq<Tracked<A>> for A