pub struct VmSpace<'a> {
pub pt: PageTable<UserPtConfig>,
pub cpus: AtomicCpuSet,
pub _marker: PhantomData<&'a ()>,
}Expand description
A virtual address space for user-mode tasks, enabling safe manipulation of user-space memory.
The VmSpace type provides memory isolation guarantees between user-space and
kernel-space. For example, given an arbitrary user-space pointer, one can read and
write the memory location referred to by the user-space pointer without the risk of
breaking the memory safety of the kernel space.
§Task Association Semantics
As far as OSTD is concerned, a VmSpace is not necessarily associated with a task. Once a
VmSpace is activated (see [VmSpace::activate]), it remains activated until another
VmSpace is activated possibly by another task running on the same CPU.
This means that it’s up to the kernel to ensure that a task’s VmSpace is always activated
while the task is running. This can be done by using the injected post schedule handler
(see inject_post_schedule_handler) to always activate the correct VmSpace after each
context switch.
If the kernel otherwise decides not to ensure that the running task’s VmSpace is always
activated, the kernel must deal with race conditions when calling methods that require the
VmSpace to be activated, e.g., UserMode::execute, VmReader and VmWriter.
Otherwise, the behavior is unspecified, though it’s guaranteed not to compromise the kernel’s
memory safety.
§Memory Backing
A newly-created VmSpace is not backed by any physical memory pages. To
provide memory pages for a VmSpace, one can allocate and map physical
memory (UFrames) to the VmSpace using the cursor.
A VmSpace can also attach a page fault handler, which will be invoked to
handle page faults generated from user space.
§Verification Design
A VmSpace has a corresponding VmSpaceOwner object that is used to track its state,
and against which its invariants are stated. The VmSpaceOwner catalogues the readers and writers
that are associated with the VmSpace, and the MemView which encodes the active page table and
the subset of the TLB that covers the same virtual address space.
All proofs about the correctness of the readers and writers are founded on the well-formedness of the MemView:
open spec fn mem_view_wf(self) -> bool {
&&& self.mem_view is Some <==> self.mv_range@ is Some
// This requires that TotalMapping (mvv) = mv ∪ writer mappings ∪ reader mappings
&&& 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 Consistency
// ======================
&&& remaining_view.mappings.subset_of(total_view.mappings)
&&& remaining_view.memory.dom().subset_of(
total_view.memory.dom(),
)
// =====================
// Total View Consistency
// =====================
&&& forall|va: usize|
remaining_view.addr_transl(va) == total_view.addr_transl(
va,
)
// =====================
// Writer correctness
// =====================
&&& forall|i: int|
0 <= i < self.writers.len() as int ==> {
&&& self.writers[i].inv()
}
}
}
}Fields§
§pt: PageTable<UserPtConfig>§cpus: AtomicCpuSet§_marker: PhantomData<&'a ()>Implementations§
Source§impl<'a> VmSpace<'a>
impl<'a> VmSpace<'a>
Sourcepub open spec fn reader_requires(
&self,
vm_owner: VmSpaceOwner<'a>,
vaddr: Vaddr,
len: usize,
) -> bool
pub open spec fn reader_requires( &self, vm_owner: VmSpaceOwner<'a>, vaddr: Vaddr, len: usize, ) -> bool
{
&&& vm_owner.inv()
&&& vm_owner.active
&&& vm_owner.can_create_reader(vaddr, len)
&&& vaddr != 0 && len > 0 && vaddr + len <= MAX_USERSPACE_VADDR
&&& current_page_table_paddr_spec() == self.pt.root_paddr_spec()
}Checks the preconditions for creating a reader or writer for the given virtual address range.
Essentially, this requires that
- the invariants of the
VmSpaceandVmSpaceOwnerhold (see [VmSpaceOwner::inv_with] andVmSpaceOwner::inv); - the
VmSpaceOwneris active (via some threads or activation function); - the
VmSpaceOwnercan create a reader or writer for the given virtual address range (seeVmSpaceOwner::can_create_readerandVmSpaceOwner::can_create_writer); - the virtual address range is valid (non-zero, non-empty, and within user-space limits);
- the currently active page table is the one owned by the
VmSpace(note that this is anuninterpspec function as this is non-trackable during verification).
Sourcepub open spec fn writer_requires(
&self,
vm_owner: VmSpaceOwner<'a>,
vaddr: Vaddr,
len: usize,
) -> bool
pub open spec fn writer_requires( &self, vm_owner: VmSpaceOwner<'a>, vaddr: Vaddr, len: usize, ) -> bool
{
&&& vm_owner.inv()
&&& vm_owner.active
&&& vm_owner.can_create_writer(vaddr, len)
&&& vaddr != 0 && len > 0 && vaddr + len <= MAX_USERSPACE_VADDR
&&& current_page_table_paddr_spec() == self.pt.root_paddr_spec()
}Checks the preconditions for creating a writer for the given virtual address range.
Most of the pre-conditions are the same as those for creating a reader (see
Self::reader_requires), except that the caller must also have permission to
create a writer for the given virtual address range.
Sourcepub open spec fn reader_ensures(
&self,
vm_owner_old: VmSpaceOwner<'_>,
vm_owner_new: VmSpaceOwner<'_>,
vaddr: Vaddr,
len: usize,
r: Result<VmReader<'_>, Error>,
r_owner: Option<VmIoOwner<'_>>,
) -> bool
pub open spec fn reader_ensures( &self, vm_owner_old: VmSpaceOwner<'_>, vm_owner_new: VmSpaceOwner<'_>, vaddr: Vaddr, len: usize, r: Result<VmReader<'_>, Error>, r_owner: Option<VmIoOwner<'_>>, ) -> bool
{
&&& vm_owner_new.inv()
&&& vm_owner_new.readers == vm_owner_old.readers
&&& vm_owner_new.writers == vm_owner_old.writers
&&& r matches Ok(
reader,
) && r_owner matches Some(
owner,
) ==> {
&&& reader.inv()
&&& owner.inv_with_reader(reader)
&&& owner.mem_view is None
}
}The guarantees of the created reader or writer, assuming the preconditions are satisfied.
Essentially, this ensures that
- the invariants of the new
VmSpaceand the reader or writer hold; - the reader or writer is associated with a
VmIoOwnerthat is well-formed with respect to the reader or writer; - the reader or writer has no memory view, as the memory view will be taken from the
VmSpaceOwnerwhen the reader or writer is activated.
§Special Note
The newly created instance of VmReader and its associated VmIoOwner are not yet
activated, so the guarantees about the memory view only require that the memory view is
None. The guarantees about the memory view will be provided by the activation function
(see VmSpaceOwner::activate_reader and VmSpaceOwner::activate_writer).
We avoid mixing the creation, usage and deletion into one giant function as this would create some unnecessary life-cycle management complexities and not really help with the verification itself.
Sourcepub open spec fn writer_ensures(
&self,
vm_owner_old: VmSpaceOwner<'a>,
vm_owner_new: VmSpaceOwner<'a>,
vaddr: Vaddr,
len: usize,
r: Result<VmWriter<'a>, Error>,
r_owner: Option<VmIoOwner<'a>>,
) -> bool
pub open spec fn writer_ensures( &self, vm_owner_old: VmSpaceOwner<'a>, vm_owner_new: VmSpaceOwner<'a>, vaddr: Vaddr, len: usize, r: Result<VmWriter<'a>, Error>, r_owner: Option<VmIoOwner<'a>>, ) -> bool
{
&&& vm_owner_new.inv()
&&& vm_owner_new.readers == vm_owner_old.readers
&&& vm_owner_new.writers == vm_owner_old.writers
&&& r matches Ok(
writer,
) && r_owner matches Some(
owner,
) ==> {
&&& writer.inv()
&&& owner.inv_with_writer(writer)
&&& owner.mem_view is None
}
}The guarantees of the created writer, assuming the preconditions are satisfied.
Most of the guarantees are the same as those for creating a reader (see
Self::reader_ensures), except that the writer is associated with a VmIoOwner that is well-formed with respect to the writer.
Sourcepub exec fn new() -> r : Self
pub exec fn new() -> r : Self
r == Self::new_spec(),Creates a new VM address space.
§Verification Design
This function is marked as external_body for now as the current design does not entail
the concrete implementation details of the underlying data structure of the VmSpace.
§Preconditions
None
§Postconditions
- The returned
VmSpaceinstance satisfies the invariants ofVmSpace - The returned
VmSpaceinstance is equal to the one created by theSelf::new_specfunction, which is anuninterpfunction that can be used in specifications.
Sourcepub exec fn cursor<G: InAtomicMode>(
&'a self,
guard: &'a G,
va: &Range<Vaddr>,
) -> Result<Cursor<'a, G>, Error>
pub exec fn cursor<G: InAtomicMode>( &'a self, guard: &'a G, va: &Range<Vaddr>, ) -> Result<Cursor<'a, G>, Error>
Gets an immutable cursor in the virtual address range.
The cursor behaves like a lock guard, exclusively owning a sub-tree of the page table, preventing others from creating a cursor in it. So be sure to drop the cursor as soon as possible.
The creation of the cursor may block if another cursor having an overlapping range is alive.
Sourcepub exec fn cursor_mut<G: InAtomicMode>(
&'a self,
guard: &'a G,
va: &Range<Vaddr>,
) -> Result<CursorMut<'a, G>, Error>
pub exec fn cursor_mut<G: InAtomicMode>( &'a self, guard: &'a G, va: &Range<Vaddr>, ) -> Result<CursorMut<'a, G>, Error>
Gets an mutable cursor in the virtual address range.
The same as Self::cursor, the cursor behaves like a lock guard,
exclusively owning a sub-tree of the page table, preventing others
from creating a cursor in it. So be sure to drop the cursor as soon as
possible.
The creation of the cursor may block if another cursor having an overlapping range is alive. The modification to the mapping by the cursor may also block or be overridden the mapping of another cursor.
Sourcepub exec fn reader(&self, vaddr: Vaddr, len: usize) -> r : Result<VmReader<'a>, Error>
pub exec fn reader(&self, vaddr: Vaddr, len: usize) -> r : Result<VmReader<'a>, Error>
Tracked(owner): Tracked<&'a mut VmSpaceOwner<'a>>,
->
vm_reader_owner: Tracked<Option<VmIoOwner<'a>>>,self.reader_requires(*old(owner), vaddr, len),self.reader_ensures(*old(owner), *owner, vaddr, len, r, vm_reader_owner@),Creates a reader to read data from the user space of the current task.
Returns Err if this VmSpace is not belonged to the user space of the current task
or the vaddr and len do not represent a user space memory range.
Users must ensure that no other page table is activated in the current task during the
lifetime of the created VmReader. This guarantees that the VmReader can operate
correctly.
§Verified Properties
§Preconditions
- The
VmSpaceinvariants must hold with respect to theVmSpaceOwner, which must be active. - The range
vaddr..vaddr + lenmust represent a user space memory range. - The
VmSpaceOwnermust not have any active writers overlapping with the rangevaddr..vaddr + len.
§Postconditions
- An inactive
VmReaderwill be created with the rangevaddr..vaddr + len.
§Safety
- The function preserves all memory invariants.
- By requiring that the
VmSpaceOwnermust not have any active writers overlapping with the target range, it prevents data races between the reader and any writers.
Sourcepub exec fn writer(self, vaddr: Vaddr, len: usize) -> r : Result<VmWriter<'a>, Error>
pub exec fn writer(self, vaddr: Vaddr, len: usize) -> r : Result<VmWriter<'a>, Error>
Tracked(owner): Tracked<&mut VmSpaceOwner<'a>>,
->
new_owner: Tracked<Option<VmIoOwner<'a>>>,self.writer_requires(*old(owner), vaddr, len),self.writer_ensures(*old(owner), *owner, vaddr, len, r, new_owner@),Returns Err if this VmSpace is not belonged to the user space of the current task
or the vaddr and len do not represent a user space memory range.
Users must ensure that no other page table is activated in the current task during the
lifetime of the created VmWriter. This guarantees that the VmWriter can operate correctly.
§Verified Properties
§Preconditions
- The
VmSpaceinvariants must hold with respect to theVmSpaceOwner, which must be active. - The range
vaddr..vaddr + lenmust represent a user space memory range. - The
VmSpaceOwnermust not have any active readers or writers overlapping with the rangevaddr..vaddr + len.
§Postconditions
- An inactive
VmWriterwill be created with the rangevaddr..vaddr + len.
§Safety
- The function preserves all memory invariants.
- By requiring that the
VmSpaceOwnermust not have any active readers or writers overlapping with the target range, it prevents data races.