Hello,
On 18.04.2017 18:09, Chris Rothrock wrote:
Let me first start off with saying that Genode, Nova and VirtualBox works flawlessly - I can boot (an Intel-based machine) and go into either a command line or GUI environment. The problem is when I try using seL4. I can compile this without any errors. The ISO image is made perfectly, it boots to this image on the same hardware - but that's where it stops. One time only I was able to see the loading screen of TinyCore Linux within VirtualBox but the boot time for this took about 45 minutes and I was unable to reproduce this boot.
what you are executing is Virtualbox without any hardware assisted virtualization support. Mainly you were running Virtualbox just with the module called "Recompiler" (REM), which is based on some older Qemu version.
Solely Genode/hw on Muen (32bit VM, one vCPU) and Genode/NOVA (32/64 bit VMs and multiple vCPUs) are supported on x86 with full hardware assisted virtualization (Intel's VT-x).
I guess my first question is this - does seL4 have the necessary virtualization support for this module?
No, afaik. The supported version of Genode/seL4 is based on seL4 3.2.0.
According to [0] and [1] the required virtualization features for x86 got added later to seL4 master. Probably seL4 4.0 have the required support, if I'm not mistaken.
If so, how can I make this work reliably?
Without updating Genode/seL4 to a recent seL4 kernel version - as first step - I think you can't. So, in principle all the limitations as mentioned in the 16.08 Genode release for our Genode/seL4 support still apply [2].
[0] https://sel4.systems/pipermail/devel/2016-December/001161.html [1] https://sel4.systems/Info/Roadmap/ [2] https://genode.org/documentation/release-notes/16.08#Limitations
Regards,