Microkernels are minimal but highly flexible kernels. Both conventional and non-classical operating systems can be built on top or adapted to run on top of them. Microkernel-based architectures should particularly support extensibility and customizability, robustness including reliability and fault tolerance, protection and security. After disastrous results in the early 90's, the microkernel approach now seems to be promising, although it still bears a lot of research risks.

The L4Ka research project aims at substantiating and establishing a new methodology for system construction that helps to manage ever-increasing OS complexity and minimizes legacy dependence. Our vision is a microkernel technology that can be and is used advantageously for constructing any general or customized operating system including pervasive systems, deep-computing systems, and huge servers.

The technology should help to manage ever-increasing OS complexity, enable stepwise innovations in OS technology while preserving legacy compatibility, and lead to a widely-accepted foundation of system architecture.

Sponsored by

Pistachio

L4Ka::Pistachio is the latest L4 microkernel developed by the System Architecture Group at the University of Karlsruhe in collabo­ration with the DiSy group at the University of New South Wales, Australia. 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.

Virtualization

We research new technologies for improving the virtual machine experience, addressing microkernels, hypervisors, the perfor­mance of running commodity operating systems in virtual machines, techniques for easily accomplishing virtualization, and the application of virtual machines for solving problems.

IDL⁴

IDL⁴ is a stub-code generator for the L4 platform. It generates communication stubs from interface definitions written in a specifi­cation language such as CORBA IDL or DCE IDL. It also uses knowledge about the hardware platform and the microkernel to optimize the performance of the generated code.

Persistence

Being able to make all objects, threads, and tasks persistent (i.e., surviving shutdowns and system crashes) poses a compelling solution for people who run, e.g., long-term scientific programs or calculations. In addition, fully orthogonal persistence also opens up a yet mostly unexplored programming model where the programmer need not explicitly store any objects to stable storage. This might largely simplify program contrsuction. When dealing with persistence in L4Ka, our main concern is to design the system so that no (or very few) modifications need to make its way into the microkernel. A set of user-level servers utilizing the well-known kernel mechanisms should prove sufficient.

Hazelnut

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) complete­ly written in C++.