Genode, seL4 and VirtualBox

Alexander Boettcher alexander.boettcher at ...1...
Tue Apr 18 21:34:22 CEST 2017


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,

-- 
Alexander Boettcher
Genode Labs

http://www.genode-labs.com - http://www.genode.org

Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth




More information about the users mailing list