pub struct VmIoEntry {
pub vm_space: Option<VmSpaceId>,
pub kind: VmIoKind,
pub vaddr: Vaddr,
pub len: usize,
pub owner: VmIoOwner,
}Expand description
Per-VmIo entry in the store.
vm_space is None for VmIoOwners that have no parent VmSpace —
kernel-space readers/writers from VmReader::from_kernel_space /
VmWriter::from_kernel_space, and val_owners produced by
read. Some(vs) for entries created by VmSpace::reader /
writer.
View state is fully determined by vm_space + kind:
Some(_)(userspace, Fallible):mem_view: None, exactly asVmSpace::reader/writerensure (vm_space.rs:323/382). Fallible methods are handle-only — no owner-side activation step exists or is needed.None && Reader(kernel reader):read_view_initialized(), perVmReader<Infallible>::from_kernel_spaceensures.None && Writer(kernel writer orconsumed_wval_owner fromread):has_write_view(), perfrom_kernel_space/ [io::read_step] ensures.
Fields§
§vm_space: Option<VmSpaceId>§kind: VmIoKind§vaddr: Vaddr§len: usize§owner: VmIoOwnerImplementations§
Source§impl VmIoEntry
impl VmIoEntry
Sourcepub open spec fn inv(self) -> bool
pub open spec fn inv(self) -> bool
{
&&& self.owner.inv()
&&& match self.vm_space {
Some(_) => self.owner.mem_view is None,
None => {
match self.kind {
VmIoKind::Reader => self.owner.read_view_initialized(),
VmIoKind::Writer => self.owner.has_write_view(),
}
}
}
}Per-entry invariant: derives view state from vm_space + kind.
Sourcepub open spec fn is_kernel_reader(self) -> bool
pub open spec fn is_kernel_reader(self) -> bool
{
&&& self.vm_space is None
&&& self.kind == VmIoKind::Reader
}Operand-typing for the Infallible read/write ops. Exec
VmReader::<Infallible>::read / VmWriter::<Infallible>::write
are typed on kernel (Infallible) reader/writer handles; the
embedding proxies “kernel/Infallible” with vm_space is None and
reader-vs-writer with kind. These are not runtime preconditions
— a userspace (Fallible) handle simply cannot be passed where the
type system demands a kernel one — so they read as a
well-formedness check on the operand, not a checkable obligation.
(inv already gives read_view_initialized / has_write_view
for these cases, exactly what vm_reader_read_embedded consumes.)
Sourcepub open spec fn is_kernel_writer(self) -> bool
pub open spec fn is_kernel_writer(self) -> bool
{
&&& self.vm_space is None
&&& self.kind == VmIoKind::Writer
}