[okl4-developer] can you please help?

[Gernot Heiser]

>>>>> On Thu, 11 Oct 2007 10:19:50 -0400, "Jorge Torres" <jorge.torres.maldonado at gmail.com> said:
JT> Hi Jothi,

JT>     1. why OKL4 Microkernel?

OKL4-> most advanced OpenSource L4 implementation embedded targeted.

JT>     2. why LEON Processor and is there any processor which i can be replaced?

JT> LEON, because  its is a simple as you getting your self a virtex development
JT> board, download it, sintetize it, "burn it", and you're ready to get your
JT> hands dirty, plus it is extremely well documented. But there should be some
JT> other interesting Open Source processors out there.

JT>     3.What will be the benefit of this project?

JT> Faster MIcrokernel, you could target it to OKL4 paravirtualization
JT> capabilities,

This isn't really the right list for this sort of discussion,
however...

Obviously I like the idea of people doing research with L4, and the
LEON would seem a good basis for architecture experiments.  But I'd
like to caution about this particular topic. Every now and then
someone suggests putting L4 functionality into hardware. However,
based on my understanding of computer architecture (and I don't claim
to be an expert) my back-of-the-envelope calculations could never come
up with a significant potential for performance improvements through
putting kernel functionality into HW, but there's clearly a loss of
flexibility.

This doesn't mean that L4 couldn't benefit from better architectural
support, but that's different. Things that come to mind:

 - ASID-tagged TLBs speed up context switches. Any architecture other
   than x86 has this anyway.

 - fast kernel entry without a trap. This has been done extremely well
   on Itanium, their guard pages allow you to get in and out of the
   kernel in a single cycle. Retrofitting this approach into RISC
   architectures would be interesting. Haven't thought about possible
   impediments.

 - support for sharing via virtually-indexed caches and a separation
   of protection from translation (along the lines of the,
   unfortunately, abandoned Voodoo architecture). AKA ARM9 done right.

 - generalised hardware-walked page tables based on a GPT structure,
   that could be used to support the Cspace data structure in seL4.

Gernot