L4 microkernel family
L4, like its predecessor microkernel L3, was created by German computer scientist Jochen Liedtke as a response to the poor performance of earlier microkernel-based OSes.
Liedtke felt that a system designed from the start for high performance, rather than other goals, could produce a microkernel of practical use.
His original implementation in hand-coded Intel i386-specific assembly language code in 1993 created attention by being 20 times faster than Mach.
For example, to implement a secure Unix-like system, servers must provide the rights management that Mach included inside the kernel.
[citation needed] While this somewhat ameliorated the performance issues, it plainly violates the minimality concept of a true microkernel (and squanders their major advantages).
Detailed analysis of the Mach bottleneck indicated that, among other things, its working set is too large: the IPC code expresses poor spatial locality; that is, it results in too many cache misses, of which most are in-kernel.
L3, developed in 1988, proved itself a safe and robust operating system, used for many years for example by Technischer Überwachungsverein (Technical Inspection Association).
As a proof of concept that a high performance microkernel could also be constructed in a higher level language, the group developed L4Ka::Hazelnut, a C++ version of the kernel that ran on IA-32- and ARM-based machines.
The effort was a success, performance was still acceptable, and with its release, the pure assembly language versions of the kernels were effectively discontinued.
This was considered necessary because L4/Fiasco is used as the basis of DROPS,[6] a hard real-time computing capable operating system, also developed at the TU Dresden.
However, the complexities of a fully preemptible design prompted later versions of Fiasco to return to the traditional L4 approach of running the kernel with interrupts disabled, except for a limited number of preemption points.
version 4) in early 2001, the System Architecture Group at the University of Karlsruhe implemented a new kernel, L4Ka::Pistachio, completely from scratch, now with focus on both high performance and portability.
[8] The group has also demonstrated that device drivers can perform equally well at user-level as in-kernel,[9] and developed Wombat, a highly portable version of Linux on L4 that runs on x86, ARM, and MIPS processors.
It was for use in commercial embedded systems, and consequently the implementation trade-offs favored small memory size and reduced complexity.
The API was modified to keep almost all system calls short enough that they need no preemption points in order to ensure high real-time responsiveness.
More recent versions are closed source and based on a rewrite to support a native hypervisor variant named the OKL4 Microvisor.
To ease meeting the sometimes conflicting requirements of performance and verification, the team used a middle-out software process starting from an executable specification written in the language Haskell.
[20] The NICTA team also proved correctness of the translation from the programming language C to executable machine code, taking the compiler out of the trusted computing base of seL4.
seL4 is also the first published protected-mode OS kernel with a complete and sound worst-case execution time (WCET) analysis, a prerequisite for its use in hard real-time computing.
[26] DARPA also funded several Small Business Innovative Research (SBIR) contracts related to seL4 under a program started by John Launchbury.
Small businesses receiving an seL4-related SBIR included: DornerWorks, Techshot, Wearable Inc, Real Time Innovations, and Critical Technologies.
[33][34] F9 microkernel,[35] a BSD-licensed L4 implementation, is dedicated to ARM Cortex-M processors for deeply embedded devices with memory protection.
