seL4_projects_libs
seL4_projects_libs copied to clipboard
sel4vm: Remove vspace dependency
This is a breaking change but is probably worthwhile to consider:
Removing the vspace_t dependency from libsel4vm and libsel4vmmplatsupport and interacting with the vspace objects directly mostly resolves a series of issues and don't really introduce any significant new problems for guests or a client vmm other than needing to update vmm drivers that expect to use the vspace objects. It also provides a reasonably small stepping stone for eventually removing more of sel4_libs as discussed recently (https://sel4.discourse.group/t/sel4-virtualization-support-current-efforts/665/3)
vspace_t is an abstraction that wraps seL4 vspace objects and provides the following functionality:
- Mapping intermediate page table objects automatically
- reserving regions for future mapping
- Helper functions for creating OS objects like ipc buffers and stacks
- Tracking reserved regions in the address space like kernel window mappings
- Unmapping vspace entries indexed by virtual address
- Creating shared mappings from one VSpace into another vspace indexed by virtual address
- Automatic placement of anonymous memory regions (eg mmap)
- Automatic allocation and mapping of any internal book-keeping data
- self-hosted or remote management of Vspaces where a vspace can refer to the current process address space or a different address space.
- A way to iteratively and dynamically map frames from another vspace into the callers vspace and call a callback function with the mapped window as an argument. The mapping is then removed when the callback returns.
Unfortunately there are the following issues:
- The book-keeping data allocation can only happen through a vspace_t instance. For book-keeping a VM's vspace, the host must then also have a vspace_t for managing its own vspace, a host may not want this level of dynamism
- The book-keeping data doesn't currently do anything clever for large frames and still keeps a unit of data for every 4k range of memory used in the vspace. So a 2MiB mapping would have 512 duplicate book-keeping entries, and a 1GiB would have 51251216bytes = 4MiB overhead.
- Encouraging implementations to use the shared-memory iterator leads to very inefficient emulated drivers as mapping and unmapping are usually more expensive than short memcpys and dominate the operation time.
The VMM only really needs features 1, 2 and 9, and it already implements its own version of region reservations (2) separately. There's also some helper functions in libsel4utils that implement just 1. and depend on a vka_t interface that the VMM also already has a copy of.
As for 6. the vmm does need a more efficient copyin/copyout mechanism that would be somewhat system specific and shouldn't create new mappings on each access.