- 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 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 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
- NICTA::Pistachio-embedded is a descendant of L4Ka::Pistachio,
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 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
- 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.
- 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.
- 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
Other Kernel Related Projects
- 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
- 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 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 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.