L4 implementations

[Gernot Heiser]

>>>>> On Fri, 8 Jun 2007 12:51:45 +1200, "Shams" <shams at orcon.net.nz> said:
S> Many thanks for the info.
S> With ERTOS I mean embedded real time OS.

S> 1. But you say it supports OKL4 supports x86 so thats means that it should
S> be possible
S> to run OKL4 on an x86-32/x86-64 server/desktop/laptop computer just like I
S> can
S> take L4.Pistaschio and run it on my 64-bit desktop computer?

Yes, but because we target embedded systems there isn't a lot of
emphasis on making everything work on standard PC platforms. Specific
questions are best directed to the OKL4 developers mailing list, see
http://portal.ok-labs.com/

S> 2. Is seL4 only for embedded systems? I mean when OKL4 incorporates
S> seL4 would these seL4 features also be available on OKL4 for x86-32/x86-64?

Sure. These features are generally independent of the processor
architecture. Once rolled out in OKL4, the features will be available
on all supported architectures. There are a large number of embedded
systems using x86 processors :-)

However, the seL4 prototype (to be released once we beat sense into
NICTA lawyers) presently only supports ARM.

S> 3. Also briefly why did OK choose seL4 rather than L4.Sec for OKL4?

Open Kernel Labs grew out of NICTA, and seL4 is a NICTA project, so
that's natural. seL4 was started at about the same time as L4.Sec, but
if you look at it you'll see that they go quite different ways. seL4
is a much more radical approach, where L4.Sec is relatively
incremental. Obviously we think that the seL4 approach is better ;-)
but judge for yourself.

Although I admit that checking is a bit difficult given the lack of a
release. But check out the several papers written about it, see
http://ertos.nicta.com.au/research/sel4/

Gernot