Hi Gernot,

> The moral successor of Pistachio as well as the open-source version of OKL4 is seL4.

I was not aware that seL4 is open source. If this is so, where is the source code available?

Thanks!
Bryce


On Tue, Mar 4, 2014 at 11:07 PM, Gernot Heiser <gernot@unsw.edu.au> wrote:
On 5 Mar 2014, at 14:42 , Taylor Bioniks <zeitue@gmail.com> wrote:

How does OKL4 compare with L4::Pistachio as far as speed, security, responsiveness?

Note that you’re talking about two systems that have been unmaintained unmaintained for years: Pistachio has lost it’s supporter base and OKL4 went closed-source. Both were as fast as it gets at their peak (http://l4hq.org/docs/performance.php). The moral successor of Pistachio as well as the open-source version of OKL4 is seL4.

L4::Pistachio uses kickstart to load it, the core kernel is contained in kernel, and the physical memory manager is stored in sigma0, I'm not even sure if it has a virtual memory manager.

Does OKL4 have a built in memory manager, and does it handle virtual memory?

Both handled VM by allowing user level to map PM into address spaces. The model differs somewhat. You’ll find descriptions of either model in week-1/2 slides of vintage editions of our Advanced OS course (http://www.cse.unsw.edu.au/~cs9242/).

Gernot


_______________________________________________
l4-hackers mailing list
l4-hackers@os.inf.tu-dresden.de
http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers