pub struct VmSpace<'a> {
pub pt: PageTable<UserPtConfig>,
pub shared_reader: bool,
pub readers: Vec<&'a VmReader<'a>>,
pub writers: Vec<&'a VmWriter<'a>>,
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, [VmSpace::reader],
[VmSpace::writer]. 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.
Fields§
§pt: PageTable<UserPtConfig>Whether we allow shared reading.
readers: Vec<&'a VmReader<'a>>All readers belonging to this VM space.
writers: Vec<&'a VmWriter<'a>>All writers belonging to this VM space.
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
{
&&& self.inv()
&&& vm_owner.inv_with(*self)
&&& vm_owner.inv()
&&& vm_owner.active
&&& vm_owner.can_create_reader(vaddr, len)
&&& vaddr != 0 && len > 0 && vaddr + len <= MAX_USERSPACE_VADDR_SPEC()
&&& 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
{
&&& self.inv()
&&& vm_owner.inv_with(*self)
&&& vm_owner.inv()
&&& vm_owner.active
&&& vm_owner.can_create_writer(vaddr, len)
&&& vaddr != 0 && len > 0 && vaddr + len <= MAX_USERSPACE_VADDR_SPEC()
&&& current_page_table_paddr_spec() == self.pt.root_paddr_spec()
}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
}
}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
}
}Sourcepub exec fn new() -> r : Self
pub exec fn new() -> r : Self
r == Self::new_spec(),r.inv(),Creates a new VM address space.
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 activate_reader(&mut self, reader: &'a VmReader<'a>)
pub exec fn activate_reader(&mut self, reader: &'a VmReader<'a>)
Tracked(vm_space_owner): Tracked <& 'a mut VmSpaceOwner <'a>>,
Tracked(owner_r): Tracked <& 'a mut VmIoOwner <'a>>,old(self).inv(),old(vm_space_owner)
.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(vm_space_owner).inv_with(*old(self)),old(vm_space_owner).inv(),old(vm_space_owner).active,old(owner_r).inv_with_reader(*reader),old(owner_r).mem_view is None,reader.inv(),self.inv(),self.shared_reader == old(self).shared_reader,self.readers@ == old(self).readers@.push(reader),owner_r.inv_with_reader(*reader),owner_r.mem_view
== Some(
VmIoMemView::ReadView(
&old(vm_space_owner).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.
Sourcepub exec fn activate_writer(&mut self, writer: &'a VmWriter<'a>)
pub exec fn activate_writer(&mut self, writer: &'a VmWriter<'a>)
Tracked(vm_space_owner): Tracked <& 'a mut VmSpaceOwner <'a>>,
Tracked(owner_w): Tracked <& 'a mut VmIoOwner <'a>>,old(self).inv(),old(vm_space_owner)
.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(vm_space_owner).inv_with(*old(self)),old(vm_space_owner).inv(),old(vm_space_owner).active,old(owner_w).inv_with_writer(*writer),old(owner_w).mem_view is None,writer.inv(),self.inv(),self.shared_reader == old(self).shared_reader,self.writers@ == old(self).writers@.push(writer),owner_w.inv_with_writer(*writer),owner_w.mem_view
== Some(
VmIoMemView::WriteView(
old(vm_space_owner).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.
Sourcepub exec fn create_reader(
&self,
vaddr: Vaddr,
len: usize,
) -> r : Result<VmReader<'a>, Error>
pub exec fn create_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.
Sourcepub exec fn create_writer(
self,
vaddr: Vaddr,
len: usize,
) -> r : Result<VmWriter<'a>, Error>
pub exec fn create_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.