seL4: does X server require Linux; hardware for VMs

[Norman Feske]

Hi John,

> I'd like to try running Genode on seL4.  I wasn't expecting this to get 
> into a release this soon so I'm very pleased to see it.

please don't mistake the current level of Genode's seL4 support as a
properly supported base platform. It is just a proof-of-concept that is
able to execute very simple Genode scenarios. See the section "Next
steps" of my most recent article about seL4 to get an idea about the
current limitations:

  http://genode.org/documentation/articles/sel4_part_3#Next_steps

In short, the seL4 version of Genode is not useful at the current stage.
If you like to experiment with Genode until we get there, I recommend
you to give the NOVA kernel (on x86) or the base-hw kernel (on ARM) a
try. Of course, we wish to extend our seL4 line of work to a fully
supported base platform. But since Genode's seL4 involvement is just a
hobby project of mine, I cannot give you a concrete time frame.

> Two questions, one re software, one re hardware:
> 
> Software: For applications like firefox I read that it's currently 
> necessary to run an X server.  Does that X instance (and firefox) need to 
> run on a Linux VM?

Firefox cannot be executed directly on Genode. Currently, the only way
to use it on top of Genode is to run it in a virtual machine (VMM),
e.g., with Linux as guest. On NOVA, there are two VMM available: Seoul
and VirtualBox.

> Hardware: I read on the seL4 FAQ that to "run Linux on top of SeL4", I 
> need:
> 
> 1. Intel VT-x with EPT (standard by now I guess?)
> 2. an HPET [1] that supports MSI delivery [2]
> 
> 
> Re 2.: is all this integrated in Haswell processors?  If yes, does Haswell 
> support this?  If no, does anybody know how to verify a motherboard 
> supports it?

Those features are fairly standard nowadays.

However, please note that Genode does not support seL4's virtualized
Linux so far. Enabling this VMM solution on Genode would require
additional work.

Best regards
Norman

-- 
Dr.-Ing. Norman Feske
Genode Labs

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

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