VmSpaceOwner

ostd::mm::vm_space::vm_space_specs

Struct VmSpaceOwner 

Source 
pub struct VmSpaceOwner<'a> {
    pub page_table_owner: OwnerSubtree<UserPtConfig>,
    pub active: bool,
    pub readers: Seq<VmIoOwner<'a>>,
    pub writers: Seq<VmIoOwner<'a>>,
    pub mem_view: Option<MemView>,
    pub mv_range: Ghost<Option<MemView>>,
    pub shared_reader: bool,
}
Expand description

A tracked struct for reasoning about verification-only properties of a VmSpace.

This struct serves as a bookkeeper for all active readers/writers within a specific virtual memory space. It maintains a holistic view of the memory range covered by the VM space it is tracking using a [Ghost<MemView>]. It also maintains a [Tracked<MemView>] for the current memories it is holding permissions for, which is a subset of the total memory range.

The management of each reader/writer and their corresponding memory views and permissions must talk to this struct’s APIs for properly taking and returning permissions, which ensures the consistency of the overall VM space so that, e.g., no memory-aliasing will occur during the lifetime of the readers/writers, and that no reader/writer will be created out of thin air without the permission from the VM space owner (or the verification rejects invalid requests).

§Lifecycle of a reader/writer

We briefly introduce how we manage the lifecycle of a reader/writer under the management of VmSpaceOwner in this section. In the first place we require that whenever the reader or writer is being used to read or write memory, a matching permission called VmIoOwner must be present. Thus the key is to properly manage the creation and deletion of the VmIoOwner.

  1. Creation: To create a new reader/writer, we first check if the new reader/writer can be created under the current VM space owner using the APIs Self::can_create_reader and Self::can_create_writer. Interestingly, this creates an empty reader/writer that doesn’t hold any memory view yet.
  2. Activation: This is the magic step where we assign a memory view to the reader/writer. Via Self::activate_reader and Self::activate_writer, the permissions will be moved from the VM space owner to the reader/writer. Note that readers do not need owned permissions so they just borrow the memory view from the VM space owner, while writers need to take the ownership of the memory view from the VM space owner. After this step, the reader/writer is fully activated and can be used to read/write memory.
  3. Disposal: After the reader/writer finishes the reading/writing operation, we can dispose it via Self::dispose_reader and Self::dispose_writer. This step is the reverse of activation, where the permissions will be moved back from the reader/writer to the VM space owner. After this step, the reader/writer is considered disposed but re-usable as long as it is properly activated again before use.
  4. Removal: If we know for sure that the reader/writer will never be used again, we can remove it from the active list via Self::remove_reader and Self::remove_writer.

Fields§

§page_table_owner: OwnerSubtree<UserPtConfig>

The owner of the page table of this VM space.

§active: bool

Whether this VM space is currently active.

§readers: Seq<VmIoOwner<'a>>

Active readers for this VM space.

§writers: Seq<VmIoOwner<'a>>

Active writers for this VM space.

§mem_view: Option<MemView>

The “actual” memory view of this VM space where some of the mappings may be transferred to the writers.

§mv_range: Ghost<Option<MemView>>

This is the holistic view of the memory range covered by this VM space owner.

§shared_reader: bool

Whether we allow shared reading.

Implementations§

Source§

impl<'a> VmSpaceOwner<'a>

Source

pub open spec fn mem_view_wf(self) -> bool

{
    &&& self.mem_view is Some <==> self.mv_range@ is Some
    &&& self
        .mem_view matches Some(
        remaining_view,
    ) ==> self
        .mv_range@ matches Some(
        total_view,
    ) ==> {
        &&& remaining_view.mappings_are_disjoint()
        &&& remaining_view.mappings.finite()
        &&& total_view.mappings_are_disjoint()
        &&& total_view.mappings.finite()
        &&& remaining_view.mappings.subset_of(total_view.mappings)
        &&& remaining_view.memory.dom().subset_of(total_view.memory.dom())
        &&& forall |va: usize| {
            remaining_view.addr_transl(va) == total_view.addr_transl(va)
        }
        &&& forall |i: int| {
            0 <= i < self.writers.len() as int
                ==> {
                    let writer = self.writers[i];
                    &&& writer
                        .mem_view matches Some(
                        VmIoMemView::WriteView(writer_mv),
                    ) && {
                        &&& forall |va: usize| {
                            &&& writer_mv.mappings.finite()
                            &&& writer_mv.addr_transl(va) == total_view.addr_transl(va)
                            &&& writer_mv
                                .addr_transl(
                                    va,
                                ) matches Some(
                                _,
                            ) ==> {
                                &&& remaining_view.addr_transl(va) is None
                                &&& !remaining_view.memory.contains_key(va)

                            }

                        }
                        &&& writer_mv.mappings.disjoint(remaining_view.mappings)
                        &&& writer_mv.mappings.subset_of(total_view.mappings)
                        &&& writer_mv.memory.dom().subset_of(total_view.memory.dom())

                    }

                }
        }
        &&& forall |i: int| {
            0 <= i < self.readers.len() as int
                ==> {
                    let reader = self.readers[i];
                    &&& reader
                        .mem_view matches Some(
                        VmIoMemView::ReadView(reader_mv),
                    ) && {
                        forall |va: usize| {
                            &&& reader_mv.mappings.finite()
                            &&& reader_mv.addr_transl(va) == total_view.addr_transl(va)

                        }
                    }

                }
        }

    }

}

This specification function ensures that the mem_view (remaining view), mv_range (total view), and the views held by active readers and writers maintain a consistent global state.

The key properties include:

§1. Existence Invariants
  • mem_view is present if and only if mv_range is present.
§2. Structural Integrity
  • Both the remaining view and the total view must have finite memory mappings.
  • Internal mappings within each view must be disjoint (no overlapping address ranges).
§3. Global Consistency
  • Subset Relation: The remaining view’s mappings and memory domain must be subsets of the total view.
  • Translation Equality: For any virtual address (VA), the address translation in the remaining view must match the translation in the total view.
§4. Writer Invariants (Exclusive Ownership)
  • Type Verification: Every writer must hold a WriteView.
  • Translation Consistency: Writer translations must match the total view.
  • Mutual Exclusion: If a writer translates a VA, that VA must not exist in the remaining view’s translation table or memory domain.
  • Mapping Isolation: Writer mappings must be disjoint from the remaining view’s mappings and must be a subset of the total view’s mappings.
§5. Reader Invariants (Shared Consistency)
  • Type Verification: Every reader must hold a ReadView.
  • Translation Consistency: Reader translations must be consistent with the total view.
Source

pub open spec fn can_create_reader(&self, vaddr: Vaddr, len: usize) -> bool

recommends
self.inv(),
{
    &&& forall |i: int| {
        0 <= i < self.writers.len()
            ==> !self.writers[i].overlaps_with_range(vaddr..(vaddr + len) as usize)
    }

}

Determines whether a new reader can be safely instantiated within the VM address space.

This specification function enforces memory isolation by ensuring that the requested memory range does not intersect with the domain of any active writer.

Source

pub open spec fn can_create_writer(&self, vaddr: Vaddr, len: usize) -> bool

recommends
self.inv(),
{
    &&& forall |i: int| {
        0 <= i < self.readers.len()
            ==> !self.readers[i].overlaps_with_range(vaddr..(vaddr + len) as usize)
    }
    &&& forall |i: int| {
        0 <= i < self.writers.len()
            ==> !self.writers[i].overlaps_with_range(vaddr..(vaddr + len) as usize)
    }

}

Checks if we can create a new writer under this VM space owner.

Similar to [can_create_reader], but checks both active readers and writers.

Source

pub uninterp fn new_vm_io_id(&self) -> nat

recommends
self.inv(),

Generates a new unique ID for VM IO owners.

This assumes that we always generate a fresh ID that is not used by any existing readers or writers. This should be safe as the ID space is unbounded and only used to reason about different VM IO owners in verification.

Source

pub proof fn activate_reader(tracked &mut self, reader: &'a VmReader<'a>, owner_r: &'a mut VmIoOwner<'a>, )

requires
old(self)
    .mem_view matches Some(
    mv,
) && forall |va: usize| (
    old(owner_r).range@.start <= va < old(owner_r).range@.end
        ==> mv.addr_transl(va) is Some
),
old(self).inv(),
old(self).active,
old(owner_r).inv_with_reader(*reader),
old(owner_r).mem_view is None,
reader.inv(),
ensures
owner_r.inv_with_reader(*reader),
owner_r.mem_view
    == Some(
        VmIoMemView::ReadView(
            &old(self).mem_view@
                .unwrap()
                .borrow_at_spec(
                    old(owner_r).range@.start,
                    (old(owner_r).range@.end - old(owner_r).range@.start) as usize,
                ),
        ),
    ),

Activates the given reader to read data from the user space of the current task.

§Verified Properties
§Preconditions
  • The VmSpace invariants must hold with respect to the VmSpaceOwner, which must be active.
  • The reader must be well-formed with respect to the VmSpaceOwner.
  • The reader’s virtual address range must be mapped within the VmSpaceOwner’s memory view.
§Postconditions
  • The reader will be added to the VmSpace’s readers list.
  • The reader will be activated with a view of its virtual address range taken from the VmSpaceOwner’s memory view.
§Safety
  • The function preserves all memory invariants.
  • The MemView invariants ensure that the reader has a consistent view of memory.
  • The VmSpaceOwner invariants ensure that the viewed memory is owned exclusively by this VmSpace.
Source

pub proof fn activate_writer(tracked &mut self, writer: &'a VmWriter<'a>, owner_w: &'a mut VmIoOwner<'a>, )

requires
old(self)
    .mem_view matches Some(
    mv,
) && forall |va: usize| (
    old(owner_w).range@.start <= va < old(owner_w).range@.end
        ==> mv.addr_transl(va) is Some
),
old(self).inv(),
old(self).active,
old(owner_w).inv_with_writer(*writer),
old(owner_w).mem_view is None,
writer.inv(),
ensures
owner_w.inv_with_writer(*writer),
owner_w.mem_view
    == Some(
        VmIoMemView::WriteView(
            old(self).mem_view@
                .unwrap()
                .split_spec(
                    old(owner_w).range@.start,
                    (old(owner_w).range@.end - old(owner_w).range@.start) as usize,
                )
                .0,
        ),
    ),

Activates the given writer to write data to the user space of the current task.

§Verified Properties
§Preconditions
  • The VmSpace invariants must hold with respect to the VmSpaceOwner, which must be active.
  • The writer must be well-formed with respect to the [VmSpaceOwner].
  • The writer’s virtual address range must be mapped within the VmSpaceOwner’s memory view.
§Postconditions
  • The writer will be added to the VmSpace’s writers list.
  • The writer will be activated with a view of its virtual address range taken from the VmSpaceOwner’s memory view.
§Safety
  • The function preserves all memory invariants.
  • The MemView invariants ensure that the writer has a consistent view of memory.
  • The VmSpaceOwner invariants ensure that the viewed memory is owned exclusively by this VmSpace.
Source

pub proof fn remove_reader(tracked &mut self, idx: int)

requires
old(self).inv(),
old(self).active,
old(self).mem_view is Some,
0 <= idx < old(self).readers.len() as int,
ensures
self.inv(),
self.active == old(self).active,
self.shared_reader == old(self).shared_reader,
self.readers == old(self).readers.remove(idx),

Removes the given reader from the active readers list.

§Verified Properties
§Preconditions
  • The VmSpace invariants must hold with respect to the VmSpaceOwner, which must be active.
  • The index idx must be a valid index into the active readers list.
§Postconditions
  • The reader at index idx will be removed from the active readers list.
  • The invariants of the VmSpaceOwner will still hold after the removal
Source

pub proof fn remove_writer(tracked &mut self, idx: usize)

requires
old(self).inv(),
old(self).active,
old(self).mem_view is Some,
old(self).mv_range@ is Some,
0 <= idx < old(self).writers.len() as int,
ensures
self.inv(),
self.active == old(self).active,
self.shared_reader == old(self).shared_reader,
self.writers == old(self).writers.remove(idx as int),

Removes the given writer from the active writers list.

§Verified Properties
§Preconditions
  • The VmSpace invariants must hold with respect to the VmSpaceOwner, which must be active.
  • The index idx must be a valid index into the active writers list.
§Postconditions
  • The writer at index idx will be removed from the active writers list.
  • The memory view held by the removed writer will be returned to the VM space owner, ensuring that the overall memory view remains consistent.
  • The invariants of the VmSpaceOwner will still hold after the removal.
Source

pub proof fn dispose_reader(tracked &mut self, tracked owner: VmIoOwner<'a>)

requires
owner.inv(),
old(self).inv(),
old(self).active,
old(self)
    .mv_range@ matches Some(
    total_view,
) && owner
    .mem_view matches Some(
    VmIoMemView::ReadView(mv),
) && old(self)
    .mem_view matches Some(
    remaining,
) && mv.mappings.finite()
    && {
        forall |va: usize| {
            &&& total_view.addr_transl(va) == mv.addr_transl(va)
            &&& mv.mappings.finite()

        }
    },
forall |i: int| 0 <= i < old(self).writers.len() ==> old(self).writers[i].disjoint(owner),
forall |i: int| 0 <= i < old(self).readers.len() ==> old(self).readers[i].disjoint(owner),
ensures
self.inv(),
self.active == old(self).active,
self.shared_reader == old(self).shared_reader,
owner.range@.start < owner.range@.end ==> self.readers == old(self).readers.push(owner),

Disposes the given reader, releasing its ownership on the memory range.

This does not mean that the owner is discarded; it indicates that someone who finishes the reading operation can let us reclaim the permission. The deletion of the reader is done via another API VmSpaceOwner::remove_reader.

Typically this API is called in two scenarios:

  1. The reader has been created and we immediately move the ownership into us.
  2. The reader has finished the reading and need to return the ownership back.
Source

pub proof fn dispose_writer(tracked &mut self, tracked owner: VmIoOwner<'a>)

requires
old(self).inv(),
old(self).active,
owner.inv(),
old(self)
    .mv_range@ matches Some(
    total_view,
) && owner
    .mem_view matches Some(
    VmIoMemView::WriteView(mv),
) && old(self)
    .mem_view matches Some(
    remaining,
) && mv.mappings.finite()
    && {
        &&& forall |va: usize| {
            &&& mv.addr_transl(va) == total_view.addr_transl(va)
            &&& mv
                .addr_transl(
                    va,
                ) matches Some(
                _,
            ) ==> {
                &&& remaining.addr_transl(va) is None
                &&& !remaining.memory.contains_key(va)

            }

        }
        &&& mv.mappings.disjoint(remaining.mappings)
        &&& mv.mappings.subset_of(total_view.mappings)
        &&& mv.memory.dom().subset_of(total_view.memory.dom())

    },
forall |i: int| {
    0 <= i < old(self).writers.len() as int ==> old(self).writers[i].disjoint(owner)
},
forall |i: int| {
    0 <= i < old(self).readers.len() as int ==> old(self).readers[i].disjoint(owner)
},
ensures
self.inv(),
self.active == old(self).active,
self.shared_reader == old(self).shared_reader,
owner.range@.start < owner.range@.end ==> self.writers == old(self).writers.push(owner),

Disposes the given writer, releasing its ownership on the memory range.

This does not mean that the owner is discarded; it indicates that someone who finishes the writing operation can let us reclaim the permission.

The deletion of the writer is through another API VmSpaceOwner::remove_writer.

Trait Implementations§

Source§

impl<'a> Inv for VmSpaceOwner<'a>

Source§

open spec fn inv(self) -> bool

{
    &&& self.page_table_owner.inv()
    &&& self.active
        ==> {
            &&& self.mem_view_wf()
            &&& self
                .mem_view matches Some(
                mem_view,
            ) ==> {
                &&& forall |i: int| {
                    0 <= i < self.readers.len() as int
                        ==> {
                            &&& self.readers[i].inv()

                        }
                }
                &&& forall |i: int| {
                    0 <= i < self.writers.len() as int
                        ==> {
                            &&& self.writers[i].inv()

                        }
                }
                &&& forall |i, j: int| {
                    0 <= i < self.readers.len() as int
                        && 0 <= j < self.writers.len() as int
                        ==> {
                            let r = self.readers[i];
                            let w = self.writers[j];
                            r.disjoint(w)
                        }
                }
                &&& !self.shared_reader
                    ==> forall |i, j: int| {
                        0 <= i < self.readers.len() as int
                            && 0 <= j < self.readers.len() as int && i != j
                            ==> {
                                let r1 = self.readers[i];
                                let r2 = self.readers[j];
                                r1.disjoint(r2)
                            }
                    }
                &&& forall |i, j: int| {
                    0 <= i < self.writers.len() as int
                        && 0 <= j < self.writers.len() as int && i != j
                        ==> {
                            let w1 = self.writers[i];
                            let w2 = self.writers[j];
                            w1.disjoint(w2)
                        }
                }

            }

        }

}

Defines the invariant for VmSpaceOwner.

This specification ensures the consistency of the VM space, particularly regarding memory access permissions and overlapping ranges.

§Invariants
  1. Recursion: The underlying page_table_owner must satisfy its own invariant.
  2. Finiteness: The sets of readers and writers must be finite.
  3. Active State Consistency: If the VM space is marked as active:
    • ID Separation: A handle ID cannot be both a reader and a writer simultaneously.
    • Element Validity: All stored VmIoOwner instances must be valid and their stored ID must match their map key.
    • Memory Isolation (Read-Write): No Reader memory range may overlap with any Writer memory range.
    • Memory Isolation (Write-Write): No Writer memory range may overlap with any other Writer memory range.
    • Conditional Read Isolation: If shared_reader is set, Readers must be mutually disjoint (cannot overlap).

Auto Trait Implementations§

§

impl<'a> Freeze for VmSpaceOwner<'a>

§

impl<'a> !RefUnwindSafe for VmSpaceOwner<'a>

§

impl<'a> Send for VmSpaceOwner<'a>

§

impl<'a> Sync for VmSpaceOwner<'a>

§

impl<'a> Unpin for VmSpaceOwner<'a>

§

impl<'a> UnwindSafe for VmSpaceOwner<'a>

Blanket Implementations§

Source§

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

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

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

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

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

Source§

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

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

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

Source§

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

Source§

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

Source§

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

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

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>

Source§

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

Source§

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

The type returned in the event of a conversion error.
Source§

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>