Kernel Implementations

OKL4

OKL4 is a descendant and successor of NICTA::Pistachio-embedded and is developed and commercially supported by Open Kernel Labs (OK). It supports a growing list of architectures and is scalable from embedded to large multi-processor enterprise systems. OKL4 features dramatically reduced overall kernel memory usage, resource control by restricting system calls that consume kernel memory, and improved communication control. On ARMv5 processors it features advanced MMU support enabling faster context switching as well as significant pagetable memory savings.

L4Ka::Pistachio

L4Ka::Pistachio is the latest L4 microkernel developed by the System Architecture Group at the University of Karlsruhe in collaboration with the DiSy group at the University of New South Wales, Australia (the ERTOS program at NICTA). It is the first available kernel implementation of the L4 Version 4 kernel API (currently code-named Version X.2), which is fully 32- and 64-bit clean, provides multiprocessor support, and super-fast local IPC.

Fiasco

Fiasco is a µ-kernel implementation for x86 with an L4 binary interface done by Michael Hohmuth. Fiasco is designed as a preemptible real-time kernel, and is used as a base for the DROPS system.

NICTA::Pistachio-embedded

NICTA::Pistachio-embedded is a descendant of L4Ka::Pistachio, optimised for use in embedded systems. It was developed by the NICTA ERTOS group. Modifications are aimed at reducing kernel complexity and memory footprint. It is superseded by OKL4 and no longer maintained.

L4Ka::Hazelnut

L4Ka::Hazelnut was designed to be portable across 32bit platforms. We separated general code like IPC, thread management, and scheduling from platform dependent code like pagetable management and exception handling. L4Ka::Hazelnut is (almost) completely written in C++. With the release of L4Ka::Pistachio development on the kernel is discontinued.

L4/Alpha

The DiSy group at UNSW developed an Alpha L4 implementation based on the Version-2 API. The kernel was based on initial work done at Dresden. With the release of L4Ka::Pistachio development on the kernel is discontinued. The NICTA group maintains the Alpha architecture of the L4Ka::Pistachio kernel.

L4/MIPS

The DiSy group at UNSW developed a 64bit MIPS L4 implementations based on the Version 2 API. The MIPS kernel was used heavily for teaching and research. With the release of L4Ka::Pistachio development on the kernel is discontinued. The NICTA group maintains the MIPS architecture of the L4Ka::Pistachio kernel.

L4/PowerPC

The L4/PowerPC is part of an attempt to use an L4 microkernel as the basis for the kernel in the field of Integrated Modular Avionics (IMA).

Other Kernel Related Projects

VFiasco

VFiasco's two primary goals are to further develop co-algebraic specification techniques such that these techniques can be applied to real software and to mechanically verify some security relevant properties of a complete microkernel operating system running on x86 PCs.

seL4

seL4 is developing a new version of the L4 AIP that matches the requirements of highly-secure embedded systems, such as strict information flow control, and strong separation of resources.

L4.verified

L4.verified aims at a complete verification of the L4 kernel, i.e. a mathematical proof that the implementation matches the specification. This includes a formalisation of the seL4 API, which will be used to prove separation and confinement properties.

Potoroo

Potoroo aims at developing a complete timing model of the L4 kernel, consisting of timing profiles of all kernel operations (which includes strict worst-case execution-time bounds). This will make L4 suitable for hard and probabilistic real-time uses.