Hi
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.
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?
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?
[1] https://en.wikipedia.org/wiki/High_Precision_Event_Timer [2] https://en.wikipedia.org/wiki/Message_Signaled_Interrupts
John
I would suspect that this will work with your processor, but features like VT-x are specific to the processor model, so you should look up your processor's specs. Also, Firefox doesn't run natively on Genode yet, so you would have to run it in a Linux VM, which should also be running an X server and a window manager.
On Thu, Sep 3, 2015 at 12:58 PM, John Lee <jjl@...348...> wrote:
Hi
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.
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?
Hardware: I read on the seL4 FAQ that to "run Linux on top of SeL4", I need:
- Intel VT-x with EPT (standard by now I guess?)
- 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?
[1] https://en.wikipedia.org/wiki/High_Precision_Event_Timer [2] https://en.wikipedia.org/wiki/Message_Signaled_Interrupts
John
Monitor Your Dynamic Infrastructure at Any Scale With Datadog! Get real-time metrics from all of your servers, apps and tools in one place. SourceForge users - Click here to start your Free Trial of Datadog now! http://pubads.g.doubleclick.net/gampad/clk?id=241902991&iu=/4140 _______________________________________________ genode-main mailing list genode-main@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/genode-main
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:
- Intel VT-x with EPT (standard by now I guess?)
- 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
On Thu, 3 Sep 2015, Norman Feske wrote:
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.
I see, thanks (and for the other answers). It's great to see such progress with both cap implementation and correctness proofs. I was starting to wonder if I'd see something I would use daily in my lifetime, now I have hope! And already something I can try right now...
John
-
John Lee -
Nobody III -
Norman Feske