1) Is there a mechanism for inter VM communication with seL4 as a
There is a vchan (virtual channel) mechanism that, in our example VMM, is used
to communicate between the VM and other components. If you had configured two
VMMs to have two VMs then if you connected both of them to vchan then the VMs
would be able to talk to each other.
2) If the VMMs run in kernel mode (PL1), as I was told, does it mean
they use hvc commands instead of swi/svc commands when sending messages
to seL4 as hypervisor?
All native seL4 threads (including the VMM) run in user mode and perform
swi/svc operations which then trap and get delivered to seL4 in hypervisor mode.
Threads such as a VM need to have a VCPU to run in modes other than user.
Devel mailing list