One of the suggestions raised at the summit last year was removing dependencies on sel4_libs from libsel4vm and libsel4vmmplatsupport.
sel4vm: Remove vspace dependency · Issue #97 · seL4/seL4_projects_libs · GitHub describes how (and why) we could remove the libsel4vspace dependency as a first step.
After that there would still be libsel4vka, libsel4simple and possibly libsel4platsupport to remove.
@kent-mcleod2 Is the idea to have a self-contained VMM, all the libraries and dependencies will move out? I will that would be nice.
One of the things I struggle a lot is with current code organization. Within libsel4vm and libsel4vmmplatsupport, interfaces between modules are not clean, and they have a lot of circular dependencies which is not easy to maintain. I think we should try to clean up those modules, but from where to start, needs to be incremental.
Originally the libsel4vm and libsel4vmm platsupport were intended to make it easier to write VMM servers as briefly described here.
There’s potentially different VMM designs depending on the virtualization use case (static vs dynamic, device drivers vs microVM, single-core vs multi-core) and taking a layered abstraction approach (where the libsel4vm tries to sit between sel4.h and the VMM application) seems to produce a lot of extra complexity not needed by some of the simpler VMM designs.
It’s probably better to focus on easy reuse of individual virtual device driver components such as vgic and virtio modules while leaving each VMM implementation to design and implement it’s own control flow and resource management for initializing and fault handling the guest OS. This would allow a reference implementation like camkes-vm to be a lot more self-contained but allow different implementations to still reuse virtual device implementations by implementing narrower interfaces that they can choose to implement.
But then again, when thinking about reusing existing virtual device components, what would it take to be able to use components from firecracker-microvm · GitHub or qemu? This is probably a completely different approach.
But then again, when thinking about reusing existing virtual device components, what would it take to be able to use components from firecracker-microvm · GitHub or qemu? This is probably a completely different approach.
As you may remember from the last summit, we at TII are working on QEMU (running on Linux VM) to provide the virtual devices for other VMs. Switching to another VMM is fairly straight forward, but of course it is not the same as running virtual device components natively. However, we’ve been also planning to build native virtual device backends by reusing crates from other Rust VMMs. This has become more and more compelling, thanks to Nick’s work with Rust support. However, we’ve mainly been thinking about targeting sel4cp.
We hope to start our experiments in the near future.