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_success_cond(self, vaddr: Vaddr, len: usize) -> bool
pub open spec fn reader_success_cond(self, vaddr: Vaddr, len: usize) -> bool
{
&&& vaddr != 0 && len > 0 && vaddr + len <= MAX_USERSPACE_VADDR
&&& current_page_table_paddr_spec() == self.pt.root_paddr_spec()
}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()
}Sourcepub open spec fn writer_success_cond(self, vaddr: Vaddr, len: usize) -> bool
pub open spec fn writer_success_cond(self, vaddr: Vaddr, len: usize) -> bool
{
&&& vaddr != 0 && len > 0 && vaddr + len <= MAX_USERSPACE_VADDR
&&& current_page_table_paddr_spec() == self.pt.root_paddr_spec()
}Source§impl<'a> VmSpace<'a>
impl<'a> VmSpace<'a>
Sourcepub exec fn new() -> r : Self
pub exec fn new() -> r : Self
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards_k): Tracked<&mut Guards<'static, KernelPtConfig>>,
Tracked(guards_u): Tracked<&mut Guards<'static, UserPtConfig>>,old(regions).inv(),Creates a new VM address space.
This allocates a new user page table by duplicating the kernel page
table’s top-level entries, and returns a VmSpace that wraps it.
§Verified Properties
§Preconditions
- Safety Invariants: The meta-region invariants must hold.
§Postconditions
Sourcepub exec fn cursor<G: InAtomicMode>(
&'a self,
guard: &'a G,
va: &Range<Vaddr>,
) -> r : Result<Cursor<'a, G>, Error>
pub exec fn cursor<G: InAtomicMode>( &'a self, guard: &'a G, va: &Range<Vaddr>, ) -> r : Result<Cursor<'a, G>, Error>
Tracked(owner): Tracked<PageTableOwner<UserPtConfig>>,
Tracked(guard_perm): Tracked<GuardPerm<'a, UserPtConfig>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards<'a, UserPtConfig>>,
->
cursor_owner: Tracked<Option<CursorOwner<'a, UserPtConfig>>>,owner.inv(),crate::mm::page_table::Cursor::<UserPtConfig, G>::cursor_new_success_conditions(va)
==> (r matches Ok(_) && cursor_owner@ matches Some(_)),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.
§Verified Properties
§Preconditions
- Safety Invariants: The page table owner must be valid.
§Postconditions
- When the virtual address range satisfies
cursor_new_success_conditions, the result isOkand aCursorOwneris returned.
Sourcepub exec fn cursor_mut<G: InAtomicMode>(
&'a self,
guard: &'a G,
va: &Range<Vaddr>,
) -> r : Result<CursorMut<'a, G>, Error>
pub exec fn cursor_mut<G: InAtomicMode>( &'a self, guard: &'a G, va: &Range<Vaddr>, ) -> r : Result<CursorMut<'a, G>, Error>
Tracked(owner): Tracked<PageTableOwner<UserPtConfig>>,
Tracked(guard_perm): Tracked<GuardPerm<'a, UserPtConfig>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards<'a, UserPtConfig>>,
->
cursor_owner: Tracked<Option<CursorOwner<'a, UserPtConfig>>>,crate::mm::page_table::Cursor::<UserPtConfig, G>::cursor_new_success_conditions(va)
==> (r matches Ok(_) && cursor_owner@ matches Some(_)),Gets a 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 by the mapping of another cursor.
§Verified Properties
§Preconditions
- Safety Invariants: The page table owner must be valid.
§Postconditions
- When the virtual address range satisfies
cursor_new_success_conditions, the result isOkand aCursorOwneris returned.
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>>,
->
reader_owner: Tracked<Option<VmIoOwner<'a>>>,old(owner).inv(),final(owner).inv(),self.reader_success_cond(vaddr, len) ==> r is Ok && reader_owner@ is Some,r is Ok && reader_owner@ is Some
==> {
&&& r.unwrap().wf(reader_owner@.unwrap())
&&& reader_owner@.unwrap().mem_view is None
},Creates a reader to read data from the user space of the current task.
Returns Err if this VmSpace is not the user space of the current task
or the vaddr and len do not represent a valid user space memory range.
§Verified Properties
§Preconditions
- The
VmSpaceOwnerinvariant must hold.
§Postconditions
- When
Self::reader_success_condholds, the result isOk. - On success, the
VmReaderand itsVmIoOwnerare well-formed with no memory view.
§Safety
- The function does not interact with the lower-level memory system directly. By checking that the target (user) page table is not the active (kernel) one, we ensure that the resulting reader cannot interact with kernel memory.
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>>,
->
writer_owner: Tracked<Option<VmIoOwner<'a>>>,old(owner).inv(),final(owner).inv(),self.writer_success_cond(vaddr, len) ==> r is Ok && writer_owner@ is Some,r is Ok && writer_owner@ is Some
==> {
&&& r.unwrap().wf(writer_owner@.unwrap())
&&& writer_owner@.unwrap().mem_view is None
},Creates a writer to write data to the user space of the current task.
Returns Err if this VmSpace is not the user space of the current task
or the vaddr and len do not represent a valid user space memory range.
§Verified Properties
§Preconditions
- The
VmSpaceOwnerinvariant must hold.
§Postconditions
- When
Self::writer_success_condholds, the result isOk. - On success, the
VmWriterand itsVmIoOwnerare well-formed with no memory view.
§Safety
- The function does not interact with the lower-level memory system directly. By checking that the target (user) page table is not the active (kernel) one, we ensure that the resulting writer cannot interact with kernel memory.