ostd::mm::vm_space

Struct VmSpaceOwner

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.

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)

                        }
                    }

                }
        }

    }

}

Source

pub open spec fn inv_with(&self, vm_space: VmSpace<'a>) -> bool

{
    &&& self.shared_reader == vm_space.shared_reader
    &&& self.readers.len() == vm_space.readers@.len()
    &&& self.writers.len() == vm_space.writers@.len()
    &&& forall |i: int| {
        0 <= i < vm_space.readers@.len() as int
            ==> {
                &&& self.readers[i].inv_with_reader(*vm_space.readers@[i])

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

            }
    }

}

The basic invariant between a VM space and its owner.

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

}

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

This requires no active writers overlapping with the new reader.

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 exec fn new_vm_io_id(&self) -> r : nat

requires

self.inv(),

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.

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:

The reader has been created and we immediately move the ownership into us.
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.

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

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

Recursion: The underlying page_table_owner must satisfy its own invariant.
Finiteness: The sets of readers and writers must be finite.
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).