L4 microkernel family
Encyclopedia
L4 is a family of second-generation microkernel
s, generally used to implement Unix-like
operating systems, but also used in a variety of other systems.
L4 was a response to the poor performance of earlier microkernel-base operating systems. German
computer scientist
Jochen 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 sparked off intense interest in the computer industry. Since its introduction, L4 has been developed for 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 widely used; Open Kernel Labs
claims deployment of one billion L4 kernels.
, Liedtke
states:
In this spirit, the L4 microkernel only provides the four basic mechanisms: address space
s, thread
s, 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 kernel
s 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.
concept used in Mach turned out to be one of the main reasons for its poor performance. This induced developers of Mach-based operating systems to move some time-critical components, like file systems or drivers, back inside the kernel. 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 spacial locality; that is, it results in too many cache
misses, of which most are in-kernel. This analysis gave rise to the principle that an efficient microkernel should be small enough such the majority of performance-critical code fits into cache (preferably a small fraction of said cache).
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
.
. 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 Thomas J. Watson Research Center
Liedtke and his colleagues continued research on L4 and microkernel based systems in general.
. This was considered necessary because L4/Fiasco is used as the basis of DROPS, a hard real-time
capable operating system, also developed at the TU Dresden.
L4/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 thread
s 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).
(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). The group has also demonstrated that user-level device drivers can perform as well as in-kernel drivers, 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.
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.
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 written in Haskell
.
seL4 is a third-generation microkernel which takes a novel approach to kernel resource management,
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,
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.Previously
cited
The NICTA group is also developing frameworks for building componentised systems on top of L4.
Osker, an OS written in Haskell
, targeted the L4 specification; although this project focused on the use of a functional programming
language for OS development, not on microkernel research per se.
Codezero, a GPL L4 microkernel targeting embedded systems is also under development, with a focus on virtualization and implementation of native OS services.
The Operating Systems Group TUD:OS of TU Dresden develops third generation microkernel-based operating
systems. The component based user-level environment L4Re
and the microkernel Fiasco.OC as well as the NOVA microhypervisor,
together with its user-level environment NUL are the results of this ongoing research.
Fiasco.OC is a third generation microkernel, which evolved from its predecessor L4/Fiasco. Fiasco.OC is capability based, supports
multi-core systems and hardware assisted virtualization. The completely redesigned user-land environment running on top of Fiasco.OC is called L4 Runtime Environment (L4Re). It provides the framework to build multi-component systems, including a client/server communication framework, common service functionality, a virtual file-system infrastructure and popular libraries such as a C library, libstdc++ and pthreads.
The platform also offers L4Linux, the multi-architecture virtualized Linux system. L4Re and Fiasco.OC run on x86 (IA32 and AMD64), ARM and PowerPC (WiP), and supersede the previous system with L4Env and L4/Fiasco.
The NOVA OS Virtualization Architecture is a research project with focus on constructing a secure and efficient virtualization environment
with a small trusted computing base. NOVA consists of a microhypervisor, a user level virtual-machine monitor, and an unprivileged componentised multi-server user environment running on top of it called NUL. NOVA runs on x86-based multi-core systems.
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.
Microkernel
In computer science, a microkernel is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system . These mechanisms include low-level address space management, thread management, and inter-process communication...
s, generally used to implement Unix-like
Unix-like
A Unix-like operating system is one that behaves in a manner similar to a Unix system, while not necessarily conforming to or being certified to any version of the Single UNIX Specification....
operating systems, but also used in a variety of other systems.
L4 was a response to the poor performance of earlier microkernel-base operating systems. German
Germany
Germany , officially the Federal Republic of Germany , is a federal parliamentary republic in Europe. The country consists of 16 states while the capital and largest city is Berlin. Germany covers an area of 357,021 km2 and has a largely temperate seasonal climate...
computer scientist
Computer scientist
A computer scientist is a scientist who has acquired knowledge of computer science, the study of the theoretical foundations of information and computation and their application in computer systems....
Jochen Liedtke
Jochen Liedtke
Jochen Liedtke was a German computer scientist, noted for his work on microkernels, especially the creation of the L4 microkernel family....
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
Intel 80386
The Intel 80386, also known as the i386, or just 386, was a 32-bit microprocessor introduced by Intel in 1985. The first versions had 275,000 transistors and were used as the central processing unit of many workstations and high-end personal computers of the time...
-specific assembly language
Assembly language
An assembly language is a low-level programming language for computers, microprocessors, microcontrollers, and other programmable devices. It implements a symbolic representation of the machine codes and other constants needed to program a given CPU architecture...
code sparked off intense interest in the computer industry. Since its introduction, L4 has been developed for platform independence and also in improving security
Computer security
Computer security is a branch of computer technology known as information security as applied to computers and networks. The objective of computer security includes protection of information and property from theft, corruption, or natural disaster, while allowing the information and property to...
, isolation, and robustness
Robustness (computer science)
In computer science, robustness is the ability of a computer system to cope with errors during execution or the ability of an algorithm to continue to operate despite abnormalities in input, calculations, etc. Formal techniques, such as fuzz testing, are essential to showing robustness since this...
.
There have been various re-implementations of the original binary L4 kernel interface (ABI
Application binary interface
In computer software, an application binary interface describes the low-level interface between an application program and the operating system or another application.- Description :...
) 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
Microkernel
In computer science, a microkernel is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system . These mechanisms include low-level address space management, thread management, and inter-process communication...
family including the L4 kernel interface
Interface (computer science)
In the field of computer science, an interface is a tool and concept that refers to a point of interaction between components, and is applicable at the level of both hardware and software...
and its different versions.
L4 is widely used; Open Kernel Labs
Open Kernel Labs
Open Kernel Labs is a privately owned company that develops microkernel-based hypervisors and operating systems for embedded systems. The company was founded in 2006 by Steve Subar and Gernot Heiser as a spinout from NICTA...
claims deployment of one billion L4 kernels.
Design paradigm
Specifying the general idea of a microkernelMicrokernel
In computer science, a microkernel is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system . These mechanisms include low-level address space management, thread management, and inter-process communication...
, Liedtke
Jochen Liedtke
Jochen Liedtke was a German computer scientist, noted for his work on microkernels, especially the creation of the L4 microkernel family....
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.
In this spirit, the L4 microkernel only provides the four basic mechanisms: address space
Address space
In computing, an address space defines a range of discrete addresses, each of which may correspond to a network host, peripheral device, disk sector, a memory cell or other logical or physical entity.- Overview :...
s, thread
Thread (computer science)
In computer science, a thread of execution is the smallest unit of processing that can be scheduled by an operating system. The implementation of threads and processes differs from one operating system to another, but in most cases, a thread is contained inside a process...
s, scheduling
Scheduling (computing)
In computer science, a scheduling is the method by which threads, processes or data flows are given access to system resources . This is usually done to load balance a system effectively or achieve a target quality of service...
, and synchronous inter-process communication
Inter-process communication
In computing, Inter-process communication is a set of methods for the exchange of data among multiple threads in one or more processes. Processes may be running on one or more computers connected by a network. IPC methods are divided into methods for message passing, synchronization, shared...
.
An operating system based on a microkernel like L4 has to provide services as servers in user space
User space
A conventional computer operating system usually segregates virtual memory into kernel space and user space. Kernel space is strictly reserved for running the kernel, kernel extensions, and most device drivers...
that monolithic kernel
Monolithic kernel
A monolithic kernel is an operating system architecture where the entire operating system is working in the kernel space and alone as supervisor mode...
s like Linux
Linux
Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...
or older generation microkernels include internally. For example, in order to implement a secure Unix-like
Unix-like
A Unix-like operating system is one that behaves in a manner similar to a Unix system, while not necessarily conforming to or being certified to any version of the Single UNIX Specification....
system, servers will have to provide the rights management that Mach
Mach (kernel)
Mach is an operating system kernel developed at Carnegie Mellon University to support operating system research, primarily distributed and parallel computation. Although Mach is often mentioned as one of the earliest examples of a microkernel, not all versions of Mach are microkernels...
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 communicationInter-process communication
In computing, Inter-process communication is a set of methods for the exchange of data among multiple threads in one or more processes. Processes may be running on one or more computers connected by a network. IPC methods are divided into methods for message passing, synchronization, shared...
concept used in Mach turned out to be one of the main reasons for its poor performance. This induced developers of Mach-based operating systems to move some time-critical components, like file systems or drivers, back inside the kernel. 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
Working set
Peter Denning defines “the working set of information W of a process at time t to be the collection of information referenced by the process during the process time interval ”. Typically the units of information in question are considered to be memory pages...
is too large: the IPC code expresses poor spacial locality; that is, it results in too many cache
CPU cache
A CPU cache is a cache used by the central processing unit of a computer to reduce the average time to access memory. The cache is a smaller, faster memory which stores copies of the data from the most frequently used main memory locations...
misses, of which most are in-kernel. This analysis gave rise to the principle that an efficient microkernel should be small enough such the majority of performance-critical code fits into cache (preferably a small fraction of said cache).
L3
Jochen LiedtkeJochen Liedtke
Jochen Liedtke was a German computer scientist, noted for his work on microkernels, especially the creation of the L4 microkernel family....
set out to prove that a well designed thinner IPC
Inter-process communication
In computing, Inter-process communication is a set of methods for the exchange of data among multiple threads in one or more processes. Processes may be running on one or more computers connected by a network. IPC methods are divided into methods for message passing, synchronization, shared...
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
L3 microkernel
L3 is a microkernel running on Intel's x86 computers. L3 is designed to be "very lean and features fast, message-based, synchronous IPC, simple-to-use external paging mechanisms and a security mechanism based on secure domains ." It is the predecessor of L4, another microkernel with similar design...
simply passed the message without any additional overhead. Defining and implementing the required security policies were considered to be duties of the user space
User space
A conventional computer operating system usually segregates virtual memory into kernel space and user space. Kernel space is strictly reserved for running the kernel, kernel extensions, and most device drivers...
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
Operating system
An operating system is a set of programs that manage computer hardware resources and provide common services for application software. The operating system is the most important type of system software in a computer system...
, used for many years for example by TÜV SÜD
TÜV SÜD
TÜV SÜD is an international service corporation focusing on consulting, testing, certification and training. At over 600 locations, primarily in Europe, North America, Asia Pacific, TÜV SÜD Group employs approximately 16,000 staff. In 2010, sales revenues totalled EUR 1.55 billion, roughly 30 per...
.
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 languageAssembly language
An assembly language is a low-level programming language for computers, microprocessors, microcontrollers, and other programmable devices. It implements a symbolic representation of the machine codes and other constants needed to program a given CPU architecture...
. 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
IBM
International Business Machines Corporation or IBM is an American multinational technology and consulting corporation headquartered in Armonk, New York, United States. IBM manufactures and sells computer hardware and software, and it offers infrastructure, hosting and consulting services in areas...
, where Liedtke started to work in 1996. At IBM's Thomas J. Watson Research Center
Thomas J. Watson Research Center
The Thomas J. Watson Research Center is the headquarters for the IBM Research Division.The center is on three sites, with the main laboratory in Yorktown Heights, New York, 38 miles north of New York City, a building in Hawthorne, New York, and offices in Cambridge, Massachusetts.- Overview :The...
Liedtke and his colleagues continued research on L4 and microkernel based systems in general.
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.L4/Fiasco
In parallel to the development of L4Ka::Hazelnut, in 1998 the Operating Systems Group TUD:OS of the TU Dresden (Dresden University of Technology) started to develop their own C++ implementation of the L4 kernel interface, called L4/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, L4/Fiasco is fully preemptible (with the exception of extremely short atomic operations) to achieve a low interrupt latencyInterrupt latency
In real-time operating systems, interrupt latency is the time between the generation of an interrupt by a device and the servicing of the device which generated the interrupt. For many operating systems, devices are serviced as soon as the device's interrupt handler is executed...
. This was considered necessary because L4/Fiasco is used as the basis of DROPS, a hard real-time
Real-time computing
In computer science, real-time computing , or reactive computing, is the study of hardware and software systems that are subject to a "real-time constraint"— e.g. operational deadlines from event to system response. Real-time programs must guarantee response within strict time constraints...
capable operating system, also developed at the TU Dresden.
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 L4/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.L4/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 thread
Alien thread
In computing, an alien thread in a multi-processor system is a thread of program execution executed by one processor on behalf of the processes running in another processor....
s 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 WalesUniversity of New South Wales
The University of New South Wales , is a research-focused university based in Kensington, a suburb in Sydney, New South Wales, Australia...
(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
Itanium
Itanium is a family of 64-bit Intel microprocessors that implement the Intel Itanium architecture . Intel markets the processors for enterprise servers and high-performance computing systems...
architecture). The group has also demonstrated that user-level device drivers can perform as well as in-kernel drivers, and developed Wombat, a highly portable version of Linux
Linux
Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...
on L4 that runs on x86, ARM and MIPS processors. On XScale
XScale
The XScale, a microprocessor core, is Intel's and Marvell's implementation of the ARMv5 architecture, and consists of several distinct families: IXP, IXC, IOP, PXA and CE . Intel sold the PXA family to Marvell Technology Group in June 2006....
processors, Wombat demonstrates context-switching costs that are up to 30 times lower than in native Linux.
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.
Current research and development
The NICTA group now focuses on the use of L4 as the basis forhighly 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
Common Criteria
The Common Criteria for Information Technology Security Evaluation is an international standard for computer security certification...
. The seL4 API is represented by an executable specification written in Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
.
seL4 is a third-generation microkernel which takes a novel approach to kernel resource management,
exporting the management of kernel resources to user
level and subjects them to the same
capability-based
Capability-based security
Capability-based security is a concept in the design of secure computing systems, one of the existing security models. A capability is a communicable, unforgeable token of authority. It refers to a value that references an object along with an associated set of access rights...
access control as user resources.
It has been formally verified,
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.Previously
cited
The NICTA group is also developing frameworks for building componentised systems on top of L4.
Osker, an OS written in Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
, targeted the L4 specification; although this project focused on the use of a functional programming
Functional programming
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...
language for OS development, not on microkernel research per se.
Codezero, a GPL L4 microkernel targeting embedded systems is also under development, with a focus on virtualization and implementation of native OS services.
The Operating Systems Group TUD:OS of TU Dresden develops third generation microkernel-based operating
systems. The component based user-level environment L4Re
and the microkernel Fiasco.OC as well as the NOVA microhypervisor,
together with its user-level environment NUL are the results of this ongoing research.
Fiasco.OC is a third generation microkernel, which evolved from its predecessor L4/Fiasco. Fiasco.OC is capability based, supports
multi-core systems and hardware assisted virtualization. The completely redesigned user-land environment running on top of Fiasco.OC is called L4 Runtime Environment (L4Re). It provides the framework to build multi-component systems, including a client/server communication framework, common service functionality, a virtual file-system infrastructure and popular libraries such as a C library, libstdc++ and pthreads.
The platform also offers L4Linux, the multi-architecture virtualized Linux system. L4Re and Fiasco.OC run on x86 (IA32 and AMD64), ARM and PowerPC (WiP), and supersede the previous system with L4Env and L4/Fiasco.
The NOVA OS Virtualization Architecture is a research project with focus on constructing a secure and efficient virtualization environment
with a small trusted computing base. NOVA consists of a microhypervisor, a user level virtual-machine monitor, and an unprivileged componentised multi-server user environment running on top of it called NUL. NOVA runs on x86-based multi-core systems.
Commercial deployment
In November 2005, NICTA announced that QualcommQualcomm
Qualcomm is an American global telecommunication corporation that designs, manufactures and markets digital wireless telecommunications products and services based on its code division multiple access technology and other technologies. Headquartered in San Diego, CA, USA...
was deploying NICTA's L4 version on their Mobile Station Modem chipsets. This led to the use of L4 in mobile phone
Mobile phone
A mobile phone is a device which can make and receive telephone calls over a radio link whilst moving around a wide geographic area. It does so by connecting to a cellular network provided by a mobile network operator...
handsets on sale from late 2006. In August 2006, ERTOS leader and UNSW professor Gernot Heiser
Gernot Heiser
Gernot Heiser is a Scientia Professor and the John Lions Chair for operating systems at the University of New South Wales . He is also leader of the at NICTA. In 2006 he co-founded Open Kernel Labs to commercialise his L4 microkernel technology...
spun out a company called Open Kernel Labs
Open Kernel Labs
Open Kernel Labs is a privately owned company that develops microkernel-based hypervisors and operating systems for embedded systems. The company was founded in 2006 by Steve Subar and Gernot Heiser as a spinout from NICTA...
(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
Dual license
Multi-licensing is the practice of distributing software under two or more different sets of terms and conditions. This may mean multiple different licenses or sets of licenses. Prefixes may be used to indicate the number of licenses used, e.g...
scheme with a Sleepycat-style
Sleepycat License
Sleepycat License is an OSI-approved open source license used by Oracle Corporation for the Berkeley DB, Berkeley DB Java Edition and Berkeley DB XML embedded database products...
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.
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 (on L4 kernel and compiler)
- Cheng Guanghui, Nicholas Mc Guire. L4/Fiasco/L4Linux Kickstart, Distributed & Embedded Systems Lab - Lanzhou University
External links
- L4Hq: L4 headquarters, community site for L4 projects
- The L4 microkernel family: Overview over L4 implementations, documentation and projects
- Official TUD:OS Wiki
- L4Ka: Implementations L4Ka::Pistachio and L4Ka::Hazelnut
- UNSW: Implementations for DEC AlphaDEC AlphaAlpha, originally known as Alpha AXP, is a 64-bit reduced instruction set computer instruction set architecture developed by Digital Equipment Corporation , designed to replace the 32-bit VAX complex instruction set computer ISA and its implementations. Alpha was implemented in microprocessors...
and MIPS architectureMIPS architectureMIPS is a reduced instruction set computer instruction set architecture developed by MIPS Technologies . The early MIPS architectures were 32-bit, and later versions were 64-bit... - OKL4: Commercial L4 version from Open Kernel Labs
- NICTA L4: Research Overview and Publications