Hello, On 2020-12-02 05:07, Andrew Warkentin wrote:
support for (presumably limited) direct system calls from VMs, bypassing any user-mode VMM (using something like Xen's trampoline page) wouldn't be accepted into seL4?
Actually, at least for ARM64, it seems you can already do seL4 system calls from VMs. This because seL4 is running in EL2 and HVC calls are already handled as system calls by seL4, judging by the source code. That said, HVC can only be called from EL1 and higher, so it has to be called by the VM kernel, not VM user space. The main problem is that you don't want VM user space to block the whole VM by doing a blocking seL4 call. Currently it does not provide a good way to receive notifications, only to send them. And interaction with IRQ delivery is tricky. Because of the above limitation it's unclear if it's worth it for our use case, so I haven't actually tried it out yet. Greetings, Indan (It seems seL4 recently changed mailing list management software, I hope that fixes the missing mail problems.) _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
