L4 microkernel family
Barry Song
L4 microkernel family
From Wikipedia, the free encyclopedia
L4 is a family of second-generation microkernels based on the original designs and implementations by German computer scientist Jochen Liedtke. Originally implemented as highly tuned Intel i386-specific assembly language code,[1] the API has seen extensive development in a number of directions, both in achieving a higher grade of platform independence and also in improving security, isolation, and robustness.
There have been various re-implementations of the original binary L4 kernel interface (ABI) and its higher level successors, including L4Ka::Pistachio (Uni Karlsruhe), L4/MIPS (UNSW) and Fiasco (TU Dresden). For this reason, the name L4 has been generalized and no longer only refers to Liedtke's original implementation. It now applies to the whole microkernel family including the L4 kernel interface and its different versions.
L4 is used in production in some mobile phones.
Contents[hide] |
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.[2]
In this spirit, the L4 microkernel only provides the four basic mechanisms: address spaces, threads, scheduling, and synchronous inter-process communication.
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.
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 one of the 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 of course, conflicted with the minimality concept of a true microkernel.
Detailed analysis of the Mach bottleneck indicated that among other things its working set is too big: there are too many cache misses and most of these are in the kernel. In other words, the code locality is poor. This raised the idea that an efficient microkernel should be small enough to fit the majority of critical sections into the processor's cache.
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.
L4
After some experience using L3, Liedtke came to the conclusion that several other Mach concepts were also misplaced. By simplifying 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 entire kernel was written in assembly language. His work caused a minor revolution in operating system design circles[citation needed]. Soon it was being studied by a number of universities and research institutes[citation needed], 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[citation needed].
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 acceptable — and with its release the pure assembly language versions of the kernels were effectively discontinued.
Fiasco
In parallel to the development of L4Ka::Hazelnut, in 1998 the operating systems group of the TU Dresden (Dresden University of Technology) started to develop their own C++ implementation of the L4 kernel interface, called Fiasco. In contrast to L4Ka::Hazelnut, which does not 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 preemptible (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.
Platform independence
L4Ka::Pistachio
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. It was released under the two-clause BSD license.
Newer Fiasco versions
The Fiasco microkernel has also been extensively improved over the years. It now supports several hardware platforms ranging from x86 through AMD64 to several ARM platforms. Notably, a version of Fiasco (FiascoUX) is able to run as a user-level application on top of Linux.
Fiasco implements several extensions to the L4v2 API. Exception IPC enables the kernel to send CPU exceptions to user-level handler applications. With the help of alien threads it is possible to perform fine-grained control over system calls. X.2-style UTCBs have been added. Furthermore, Fiasco contains mechanisms for controlling communication rights as well as kernel-level resource consumption. On top of Fiasco a collection of basic user level services are developed (called L4Env) that amongst others are used to para-virtualise current Linux version (2.6.x) (called L4Linux).
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 assembly 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).[3] The group has also demonstrated that user-level device drivers can perform as well as in-kernel drivers,[4] 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.[5]
Later the UNSW group, at their new home at NICTA, forked L4Ka::Pistachio into a new L4 version called NICTA::L4-embedded. As the name implies, this was aimed at use in commercial embedded systems, and consequently the implementation trade-offs favoured small memory footprints and aimed 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.[6]
Current research and development
The NICTA group now focuses on the use of L4 as the basis for highly-secure and -reliable systems. At the core of this approach is a new L4 kernel, called seL4, aimed at satisfying security requirements such as those of Common Criteria. The seL4 API is represented by an executable specification[7] written in Haskell.
seL4 is a third-generation microkernel which takes a novel approach to kernel resource management,[8] exporting the management of kernel resources to user level and subjects them to the same capability-based access control as user resources. It has been formally verified[9], which means that there is a (machine-checked) mathematical proof that the implementation is consistent with the specification. This provides a guarantee that the kernel is free of implementation bugs such as deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialised variables. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.[9].
The NICTA group is also developing frameworks for building componentised systems on top of L4.[10]
Osker [1], 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.
Codezero, a GPL L4 microkernel targeting embedded systems is also under development, with a focus on virtualization and implementation of native OS services.
Commercial deployment
In November 2005, NICTA announced that Qualcomm was deploying NICTA's L4 version on their Mobile Station Modem chipsets. This led 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 Labs) to support commercial L4 users and further develop L4 for commercial use, in close collaboration with NICTA. OK Labs distributes its own version of L4, called OKL4, which is descended from NICTA::L4-embedded, and is supported for x86, ARM and MIPS. OKL4 was initially distributed under a BSD license. Recent releases use a dual licensing scheme with a Sleepycat-style open-source license. OK Labs also distributes a para-virtualized Linux called OK:Linux, a descendant of Wombat, as well paravirtualized versions of SymbianOS, Android and Windows.
In April 2008, OK Labs released OKL4 2.1, which is the first public version of L4 using capability-based protection. OKL4 3.0 was released in October 2008.
References
- ^ Liedtke, Jochen (December 1993). "Improving IPC by kernel design". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 175–88. http://portal.acm.org/citation.cfm?id=168619.168633&coll=portal&dl=ACM&type=series&idx=168619&part=Proceedings&WantType=Proceedings&title=ACM%20Symposium%20on%20Operating%20Systems%20Principles&CFID=18793560&CFTOKEN=54028606.
- ^ Jochen Liedtke (December 1995). "On µ-Kernel Construction". Proc. 15th ACM symposium on Operating Systems Principles (SOSP). pp. 237–250. http://i30www.ira.uka.de/research/publications/papers/index.php?lid=en&docid=642.
- ^ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (April 2005). "Itanium—a system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp. 264–278. http://www.usenix.org/publications/library/proceedings/usenix05/tech/general/gray.html.
- ^ Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (September 2005). "User-level device drivers: achieved performance". Journal of Computer Science and Technology 5 (20): 654–664. doi:10.1007/s11390-005-0654-4.
- ^ van Schaik, Carl; Heiser, Gernot (January 2007). "High-performance microkernels and virtualisation on ARM and segmented architectures". 1st International Workshop on Microkernels for Embedded Systems. Sydney, Australia: NICTA. pp. 11–21. http://ertos.nicta.com.au/publications. Retrieved 2007-04-01.
- ^ Ruocco, Sergio (October 2008). "A Real-Time Programmer's Tour of General-Purpose L4 Microkernels". EURASIP Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications 2008: 1. doi:10.1155/2008/234710. http://www.hindawi.com/getarticle.aspx?doi=10.1155/2008/234710.
- ^ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Cock; David; Chakravarty, Manuel M. T. (September 2006). "Running the manual: an approach to high-assurance microkernel development". ACM SIGPLAN Haskell Workshop. Portland, Oregon. pp. 60–71. http://portal.acm.org/citation.cfm?id=1159842.1159850&coll=portal&dl=ACM&type=series&idx=1159842&part=Proceedings&WantType=Proceedings&title=Haskell&CFID=18785943&CFTOKEN=93152956.
- ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). "Kernel design for isolation and assurance of physical memory". 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK. doi:10.1145/1435458. http://ertos.nicta.com.au/publications/papers/Elkaduwe_DE_08.abstract.
- ^ a b Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai et al. (October 2009). "seL4: Formal verification of an OS kernel". 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA. http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf.
- ^ Kuz, Ihor; Liu, Yan; Gorton, Ian; Heiser, Gernot (to appear). "CAmkES: a component model for secure microkernel-based embedded systems". Journal of Systems and Software 80: 687. doi:10.1016/j.jss.2006.08.039.
Further reading
- Jochen Liedtke, Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, Gyula Szalay. Two years of experience with a μ-Kernel based OS, ACM Press 1991
- Liedtke, Jochen; Haeberlen, Andreas; Park, Yoonho; Reuther, Lars; Uhlig, Volkmar (2000-10-22). "Stub-Code Performance is Becoming Important" (PDF). In Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), San Diego, CA, October 2000. http://l4ka.org/publications/. Retrieved 2006-09-05. (on L4 kernel and compiler)
- Cheng Guanghui, Nicholas Mc Guire. L4/Fiasco/L4Linux Kickstart, Distributed & Embedded Systems Lab - Lanzhou University
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
- OKL4 – Commercial L4 version from Open Kernel Labs
- NICTA L4 – Research Overview and Publications
- L4Linux – Linux running on L4 microkernel
- DROPS – The Dresden Real-Time Operating System Project
- NOVA – A free L4 microkernel-based hypervisor
- Information about L3, L4's predecessor
- Codezero, A free L4 implementation in C for ARM
沈晓滨
--
You received this message because you are subscribed to the Google
Groups "Linux设备驱动开发者群落" group.
To post to this group, send email to linux...@googlegroups.com
To unsubscribe from this group, send email to
linuxdriver...@googlegroups.com
For more options, visit this group at
http://groups.google.gr/group/linuxdriver?hl=zh-CN
Barry Song
Welcome to the Open Kernel Labs Community Wiki
OKL4 is a high-performance system software platform, built using cutting-edge microkernel technology. It provides developers with the technologies and tools needed to build and deploy innovative, high-performance and secure intelligent devices.
It's absolutely free to join the Open Kernel Labs Community and immediately start using our software products as a basis for developing next-generation embedded-systems software. The content you'll find on this Wiki will serve you well in getting started with OKL4 by providing you with a repository of useful reference material and general know-how.
Please contact OK Labs at in...@ok-labs.com or call +1 312.924.1073 if you have any questions about OKL4 or are looking to get a jumpstart on a project. Additionally, you can always join the Developer Mailing list for answers to your OKL4 questions.
OKL4 3.0 Release
OKL4 3.0 is the latest release of OKL4 (October, 2008). To view other releases, check out PreviousReleases. For more information on the naming of versions, see VersioningPolicy.
Release Item |
Brief Description |
Binary |
Source |
Tutorial |
Reference |
OKL4 |
Base release of OKL4 |
|
SDK Tutorial: Hello World |
Reference Manual |
|
OKL4 on ARM926 |
Necessary support for OKL4 on ARM926 hardware platforms |
|
|
||
OKL4 on ARM1136 |
Necessary support for OKL4 on ARM1136 hardware platforms |
|
|
||
OKL4 on ARM920 |
Necessary support for OKL4 on ARM920 hardware platforms |
|
|
|
|
OKL4 on XScale |
Necessary support for OKL4 on XScale hardware platforms |
|
|
||
Linux Patches |
Patches to para-virtualize Linux on OKL4 |
|
|
||
EABI Toolchain |
Cross-compiled Linux ARM EABI toolchain |
|
|
|
|
Skyeye Simulator |
An integrated simulation environment in Linux to emulate various ARM-based and other processors. This is particularly provided for Gumstix platform |
|
|
||
QEMU Simulator |
An integrated simulation environment in Linux to emulate a wide variety of processors including x86, PowerPC, XScale, etc. Particularly, provided to support KZM and Versatile platforms |
|
|
Contribute
Get Answers
The OKL4 technical FAQ. Go>
Get Known
Your projects, thoughts, and ideas: how are you using OKL4? Go>
Get Help / Find Answers / Get Involved
If you'd like to know more or interact with like-minded people like yourself, please do join the ever growing horde of OKL4 developers active on our MailingList.
The Wiki is open and free for any community member to contribute to - we welcome you to share your experiences, projects, tips and hints as you work with OKL4. Head on over to Registration and grab a username and password.
Documentation
Simulators
To test images built using the SDK or the complete source tarball you can use one of the following simulators depending on which platform you are using.
Skyeye (for Gumstix)
A binary version of the Skyeye 1.2.1n simulator available to simulate the Gumstix platform. You will need the skyeye.conf file as well. To simulate use:
# skyeye -c skyeye.conf -e image.sim
Qemu (for KZM and Versatile)
A source copy of the Qemu 0.9.1 simulator is available to simulate the KZM and Versatile platforms. It is built with the following commands:
# ./configure --target-list=arm-softmmu --disable-sdl --static --disable-gfx-check
# make
Using the SDK
To use the SDK extract the tarball and set the OKL4_SDK_ROOT environment variable to point to that directory:
# tar zxf sdk-xscale.tar.gz
# export OKL4_SDK_ROOT=/path/to/sdk
From your project directory or from one of the examples you can use make to build your project. There are two variables that can be passed to make, KERNEL and BUILD. KERNEL can be set to micro or nano and defines which kernel the project object files are linked against. BUILD can be set to benchmark, debug, debug_no_console, production or tracebuffers and defines the level of debug support provided in the kernel. For example, to build and then link the hello world example against the nano kernel compiled for benchmarking you would use:
# cd $OKL4_SDK_ROOT/okl4/xscale/examples/singlecell
# make KERNEL=nano BUILD=benchmark
The image that is built can be found in the build directory which depends on the KERNEL and BUILD variables:
build.<KERNEL>-<BUILD>/images/image.elf
XScale
The XScale SDK supports the Gumstix platform. To simulate an image with Skyeye use:
# skyeye -c skyeye.conf -e build.<KERNEL>-<BUILD>/images/image.elf
ARM1136js
The ARM1136js SDK supports the KZM platform. To simulate an image linked against the OKL4 Microkernel use:
# qemu-system-arm -M kzm -nographic -start-addr 0x86800000 -kernel build.micro-<BUILD>/images/image.elf
whereas for an image linked against the OKL4 Nano use:
# qemu-system-arm -M kzm -nographic -kernel build.nano-<BUILD>/images/image.elf
ARM926ejs
The ARM926ejs SDK supports the Versatile platform. To simulate an image linked against the micro kernel use:
# qemu-system-arm -M versatileab -start-addr 0x07900000 -nographic -kernel build.micro-<BUILD>/images/image.elf
whereas for an image linked against the nano kernel use:
# qemu-system-arm -M versatileab -start-addr 0x04100000 -nographic -kernel build.nano-<BUILD>/images/image.elf