L4 microkernel family

From Wikipedia, the free encyclopedia

L4 is the name of a second-generation microkernel which was originally designed and implemented by Jochen Liedtke in highly tuned Intel i386-specific assembly language code. Since then the system has seen dramatic development in a number of directions, both in achieving a higher grade of platform independendence and also in improving security, isolation, and robustness. There have been various re-implementations such as L4Ka::Pistachio (Uni Karlsruhe), L4/MIPS (UNSW) or Fiasco (TU Dresden) of the original binary L4 kernel interface (ABI) and its higher level successors. For this reason, now the name L4 does not only refer to the orignal implementation by Jochen Liedtke but also to the whole microkernel family and as well to the L4 kernel interface with its different versions.

Contents 1 Design paradigm 2 History 2.1 L3 2.2 L4 2.3 L4Ka::Hazelnut 2.4 Fiasco 2.5 Platform independence: L4Ka::Pistachio and newer Fiasco versions 2.6 University of New South Wales and NICTA 3 Current research and development 4 Commercial Deployment 5 References 6 External links

[edit] Design paradigm

Specifying the general idea of a microkernel Liedtke states:

A concept is tolerated inside the microkernel only if moving it outside the kernel, i.e., permitting competing implementations, would prevent the implementation of the system's required functionality.^[1]

Therefore, the L4 microkernel only provides the 4 basic mechanisms: a thread model, a mechanism for synchronous thread communication, a basic scheduler, and an address space abstraction.

An operating system based on a microkernel like L4 has to provide services as servers in user space that monolithic kernels like Linux or older generation microkernels include internally. For example, in order to implement a secure Unix-like system, servers will have to provide the rights management that Mach included inside the kernel.

[edit] History

The realization of drawbacks in design and performance of the first-generation Mach microkernel led a number of developers to re-examine the entire microkernel concept in the mid-1990s. The asynchronous in-kernel-buffering process communication concept used in Mach turned out to be the one of main reasons for its poor performance. This induced some of the Mach developers to put some time-critical components, like file systems or drivers, back inside the kernel, which is, of course, conflicting with the minimality concept of a true microkernel.

[edit] L3

Jochen Liedtke set out to prove that a well designed thinner IPC layer, with careful attention to performance and machine-specific (as opposed to platform independent) design could yield massive real-world performance improvements. Instead of Mach's complex IPC system, his L3 microkernel simply passed the message without any additional overhead. Defining and implementing the required security policies were considered to be duties of the user space servers. The role of the kernel was only to provide the necessary mechanism to enable the user-level servers to enforce the policies. L3 proved itself a safe and robust operating system, used for many years for example by TÜV SÜD.

[edit] L4

After some experience using L3, Liedtke came to realize that several other Mach concepts were also misplaced. By simplyfying the microkernel concepts even further he developed the first L4 kernel which was primarily designed with high performance in mind. In order to wring out every bit of performance the whole kernel was written in assembly language. His work caused a minor revolution in operating system design circles. Soon it was being studied by a number of universities and research institutes, including IBM, where Liedtke started to work in 1996. At IBM's T.J. Watson Research Center Liedtke and his colleagues continued research on L4 and microkernel based systems in general.

[edit] L4Ka::Hazelnut

In 1999, Liedtke took over the Systems Architecture Group at the University of Karlsruhe, where he continued the research into microkernel systems. 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 IA32- and ARM-based machines. The effort was a success, performance was still excellent, and with its release the pure assembly language versions of the kernels were effectively discontinued.

[edit] Fiasco

In parallel to the development of L4Ka::Hazelnut, in 1998 the operating systems group of the TU Dresden (Technische Universität Dresden) started to develop their own C++ implementation of the L4 kernel interface, called Fiasco. In contrast to L4Ka::Hazelnut, which doesn't allow concurrency in the kernel at all and its successor L4Ka::Pistachio, which allows interrupts in the kernel only at specific preemption points, Fiasco is fully preemptable (with the exception of extremely short atomic operations) to achieve a low interrupt latency. This was considered necessary because Fiasco is used as the basis of DROPS, a hard real-time capable operating system, also developed at the TU Dresden.

[edit] Platform independence: L4Ka::Pistachio and newer Fiasco versions

Up until the release of L4Ka::Pistachio and newer versions of Fiasco, all L4 microkernels had been inherently tied close to the underlying CPU architecture. The next big shift in L4 development was the development of a platform independent API that still retained the high performance characteristics despite its higher level of portability. Although the underlying concepts of the kernel were the same, the new API provided many radical changes to previous L4 versions, including better support for multi-processor systems, looser ties between threads and address spaces, and the introduction of user-level thread control blocks (UTCBs) and virtual registers. After releasing the new L4 API (Version X.2 a.k.a. 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 as well as portability.

The Fiasco microkernel has also been intensivly improved over the years and has now an internal hardware abstraction.

[edit] University of New South Wales and NICTA

Development also took place at the University of New South Wales (UNSW), where developers implemented L4 on several 64-bit platforms. Their work resulted in L4/MIPS and L4/Alpha, resulting in Liedtke's original version being retroactively named L4/x86. Like Liedtke's original kernels, the UNSW kernels (written in a mixture of assembler and C) were unportable and each implemented from scratch. With the release of the highly portable L4Ka::Pistachio, the UNSW group abandoned their own kernels in favour of producing highly-tuned ports of L4Ka::Pistachio, including the fastest-ever reported implementation of message passing (36 cycles on the Itanium architecture)^[2]. The group has also demonstrated that user-level device drivers can perform as well as in-kernel drivers^[3], and developed Wombat, a highly portable version of Linux on L4 that runs on x86, ARM and MIPS processors. On XScale processors, Wombat demonstrates context-switching costs that are up to 30 times lower than in native Linux^[4].

[edit] Current research and development

Recently the UNSW group, at their new home at National ICT Australia (NICTA), forked L4Ka::Pistachio into a new L4 version called NICTA::L4-embedded. As the name implies, this is aimed at use in commercial embedded systems, and consequently the implementation tradeoffs favour small memory footprints and aim to reduce complexity. The API was modified to keep almost all system calls short enough so they do not require preemption points in order to ensure high real-time responsiveness.

The NICTA group now focuses on turning L4 into a highly-secure and -reliable platform. A formal proof of the correctness of the implementation is in progress^[5]. This is combined with the development of a new L4 API, called seL4, aimed at satisfying security requirements such as those of Common Criteria. The seL4 API is is represented by an executable specification^[6] written in Haskell. There is a similar project on performing an exhaustive analysis of the latencies of kernel operations. Further work is developing frameworks for building componentised systems on top of L4^[7].

The GNU Hurd project was considering adopting the L4 microkernel (GNU Hurd/L4 [1]) to replace Mach, but the new design will be capability-based and L4 doesn't support capabilities. Possible alternatives are the upcoming microkernels L4.sec and Coyotos, with a strong bias towards Coyotos (its development is made public, its specification published and efforts have been made to make it fit HURD's needs).

Osker [2], an OS written in Haskell, is being written to match the L4 specification; although this focuses on the use of a functional programming language for OS development, not strictly microkernel research.

[edit] Commercial Deployment

In November 2005, NICTA announced that Qualcomm was deploying NICTA's L4 version on their Mobile Station Modem chipsets. This lead to the use of L4 in mobile phone handsets on sale from late 2006. In August 2006, ERTOS leader and UNSW professor Gernot Heiser spun out a company called Open Kernel Labs (OK) to support commercial L4 users and further develop L4 for commercial use, in close collaboration with NICTA. OK's L4 version, which is descended from NICTA::L4-embedded, is called OKL4, and is distributed as open source under a BSD license.

[edit] References

[edit] External links

• L4ka publications
• L4Hq – L4 headquarters, community site for L4 projects
• The L4 microkernel family – Overview over L4 implementations, documentation and projects
• L4Ka – Implementations L4Ka::Pistachio and L4Ka::Hazelnut
• Fiasco – A free C++ implementation for x86 and ARM processors
• UNSW – Implementations for DEC Alpha and MIPS architecture
• NICTA L4 – Research Overview and Publications
  • Wombat – A Linux port on top of the L4/Iguana OS
  • Darbat – A Darwin port on top of the L4 microkernel
• L4Linux – Linux running on L4 microkernel
• DROPS – The Dresden Real-Time Operating System Project
• GNU Hurd/L4 – Port of GNU Hurd/Mach to L4
• China Comp L4 Research Group – The China Computer µKernel L4 Research Group
• Information about L3, L4's predecessor