One of the main goals of the SIG VMM is to bring together people working on seL4 virtualization support. So, feel free to reply on this thread with your current effort and/or interest area on seL4 virtualization. This will be useful for the community to know itself and be aware of possible efforts in the same direction from peers.
Some examples of interesting questions to answer when posting a reply in this thread:
What seL4 kernel “flavor” and architecture are you using (e.g., MCS ARM, non-MCS x86, etc.)?
What VMM are you working on (e.g., CAmkES, seL4CP)? What are your development plans for the VMM?
What are the topics you are working on that you believe would be necessary for improving the support at a VMM level?
What use cases are you targeting?
Is there any discussion topic you would like to raise related to seL4 virtualization?
Apart from participating in this discussion, you are also welcome to participate in the seL4 developer hangout/video calls, happening every 15 days.
What is the state of this SIG? I have started looking into the existing VMM and the pending PRs, but there has been not much feedback so far - except from the usual suspects. Dornerworks had some nice contribution recently, some still pending in PRs that are worth to pick up. @gerwin.klein recently made Github CI hardware testing work for the CAmkES VMM (thanks, this allowed me to fix the breaker I’ve introduced), and I’ve seen Ivan is working on a CP-VMM in his Github fork. There are some interesting branches in the TII forks also. What I’m missing is some interest in improving mainline (CAmkES or CP, or even a common lib code base) towards a greater open source goal.
These were the rough list of use-cases and current issues with the virtualization support discussed at the Virtualization Birds of a Feather session at the summit (notes taken by @ihor.kuz).
use cases
+ cyber retrofit
+ multi personality (e.g. multi android phone)
+ server/cloud virtualisation
+ partitioning OS (e.g. Qubes)
+ run legacy code
+ device drivers
+ sandbox untrusted code
+ attestation
current issues with vmm/lib/kernel
+ no SMC
+ sel4libs dependency
+ lack of dynamic abilities?
+ platform bringup
+ non-Linux support (not much of an issue?)
+ x64
+ SMMU
+ Gicv3
+ platform def not entirely device tree based
+ boot interface/loading images
+ device virtualisation
+ more complete virtio interfaces (and instructions)
+ how to add virtual devices (that are not virtio)
+ multiplexing access to shared devices
+ any performance issues?
+ code modularity
+ multiproc model of VMM
I agree with @axel 's perspective. It’s essential to have a broader engagement to drive the improvement of mainline VMM. Thanks @kent-mcleod2 for sharing the list of use cases and current issues discussed during the Virtualization Birds of a Feather session at the summit. I can see that the community is tackling some of those “current issues” in their projects - as @axel mentioned.
To @axel and others, do you have any suggestions on how we could foster interest in improving the mainline VMM? It would be beneficial not only to brainstorm strategies to attract more contributors but also to determine where this should be headed, generating enthusiasm around working on these crucial aspects of seL4. One approach could be to identify common ground among the various projects tackling these issues, which may help streamline our efforts, create a more unified vision for the VMM’s future development, and provide clear direction for new and existing contributors alike.
The list of new improvements or features is huge, and there is limited resources for that. I think we need to write them down in a roadmap organized by priorities.
We can think what are the current limitations, priority of new features or improvement/refactoring of the existing ones, or a combination of both.
@evermatos Think about short term plan with selected high priority improvements and features, where people can pick the parts they are interested on and work on it.
As Kent suggests anything that sparks interest would be nice to have.
