I'm working with the team at Critical Technologies and I am trying to get this combination to work - Genode with seL4 microkernel and the VirtualBox module (using TinyCore Linux).
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.
I guess my first question is this - does seL4 have the necessary virtualization support for this module? If so, how can I make this work reliably?
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,
On 4/18/17 2:34 PM, Alexander Boettcher wrote:
... 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
The combination of Genode and seL4 *is* particularly attractive. How large an effort does upgrading to seL4 4.x represent?
Would this be any easier with seL4 on the ARM platform? I guess this is not yet a supported combination, but should be possible...?
Regards, Steve Harp
We have also been putting forth the effort for Genode/seL4 on ARM with mixed success on different ARM platforms. As it stands, if we can get an ARM platform working with Genode/seL4 and especially with a VirtualBox environment this would make us very happy. I doubt this combination is even close to ready, however.
On Tue, Apr 18, 2017 at 4:09 PM, Steven Harp <steven.harp@...486...> wrote:
On 4/18/17 2:34 PM, Alexander Boettcher wrote:
... 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
The combination of Genode and seL4 *is* particularly attractive. How large an effort does upgrading to seL4 4.x represent?
Would this be any easier with seL4 on the ARM platform? I guess this is not yet a supported combination, but should be possible...?
Regards, Steve Harp
Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ genode-main mailing list genode-main@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/genode-main
-
Alexander Boettcher -
Chris Rothrock -
Steven Harp