Linux 2.4 was ported to L4Ka::Pistachio by the System Architecture Group of Universität Karlsruhe to create L4Linux-2.4. It is based on the previous L4Linux-2.2 of the Operating Systems Group of Technische Universität Dresden. Adam Lackorzynski of TU Dresden extended L4Linux-2.4 to support Dresden's microkernels and operating environments (and has also kept L4Linux current with the official Linux kernel releases).

L4Linux-2.4 supports only the IA32 platform. It supports SMP when used with the L4Ka::Pistachio microkernel. And it is kept up-to-date with the latest Linux 2.4 releases (with a slight delay).

Audience

L4Linux is for the L4 developer community. L4Linux offers a great environment in which to develop and research with L4 microkernels. It offers the support infrastructure of Linux, yet the advantages of the L4 microkernel.

Availability

Like the Linux kernel, the L4Linux kernel is available under the GPL version 2 license.

You can obtain the L4Linux-2.4 source code from our anonymous CVS server.

More general L4Linux information is available at l4linux.org.

Historical

The paper presented at the 16th ACM SOSP in 1997 entitled The Performance of µ-Kernel-Based Systems (pdf, ps) describes one of the first adaptations of Linux to L4. The paper demonstrates that it is possible to implement a high-performance conventional operating system on a microkernel, and that a high-performance microkernel is crucial to achieve this. Authors: H. Härtig, M. Hohmuth, J. Liedtke, S. Schönberg, and J. Wolter. The Linux version was 2.0.28, and the L4 microkernel was Jochen Liedtke's x86 assembler kernel (which implemented the L4 V2 API).

L4Linux on L4Ka::Pistachio

Updates

January 21, 2004

Corrected section about virtual processors.

Discussions

See the L4Ka::Pistachio page for L4Ka mailing list and IRC information. Before reporting bugs and problems, please read the Reporting Problems section below.

Compatibility

When using L4Linux-2.4 with L4Ka::Pistachio, version 0.4 or newer of L4Ka::Pistachio is required (or the latest edition from anonymous CVS).

L4Linux may support L4Ka::Hazelnut, but we have not tested such a configuration recently. L4Ka::Hazelnut is an obsoleted microkernel, in favor of L4Ka::Pistachio.

Performance

The current release of L4Linux is unoptimized. We have outstanding optimizations to be applied in future releases (such as small address spaces, and improvements in message passing). We have not yet analyzed L4Linux-2.4 for performance bottlenecks, nor memory waste.

Booting

First follow the instructions to establish a bootable L4Ka::Pistachio/ia32 environment, using the GRUB bootloader and the L4Ka::Kickstart utility.

L4Linux usually should be the roottask. The L4Linux executable is named vmlinuz.VX2. Add an entry to your GRUB menu.lst file which loads an L4Linux environment, and uses vmlinuz.VX2 file for the roottask module. An example entry for the menu.lst file:

title=L4Linux on L4Ka::Pistachio kernel=/kickstart module=/ia32-kernel module=/sigma0 module=/vmlinuz.VX2 no-scroll console=herc console=tty

GRUB permits you to specify command-line parameters for the modules, and thus you can specify traditional Linux command line parameters for the Linux kernel. The no-scroll command line parameter is optional, and disables VGA console scrolling. The no-scroll option may be desirable when using the debug version of L4Ka::Pistachio, to avoid undesirable side effects due to scrolling the spinning debug wheels displayed in the upper right of the VGA console.

If you wish to use an initial ramdisk, define another module immediately following the L4Linux module. Here is a menu.lst entry which boots from our sample ramdisk (available for download):

title=L4Linux on L4Ka::Pistachio with Debian ramdisk kernel=/kickstart module=/ia32-kernel module=/sigma0 module=/vmlinuz.VX2 no-scroll devfs=mount ramdisk_size=65536 root=/dev/ram0 rw console=herc console=tty module=/ramdisk.gz

Note that the 2.4 series of the Linux kernel integrates the ramdisk into its buffer cache, and thus makes efficient use of memory.

Sample Ramdisk

The sample ramdisk contains an elementary installation of Debian 3.0. It also contains Apache2 (the prefork version) in /usr/local/apache2-prefork (binaries and config files, while logs go to /var/log) and configured to serve files from /home/www.

The root password is pistachio

The ramdisk is configured to obtain a DHCP address on eth0. And it by default starts the web server, listening on port 80.

The ramdisk is configured to open consoles only on the VGA device. If for some reason your kernel won't support the VGA console, then init will fail trying to open the tty processes. It is not configured to start a tty on the serial interfaces, since the serial ports are often used for access to the kernel debugger of L4Ka::Pistachio.

Source Configuration and Building

We have tested and used L4Linux up to version 2.4.22. The CVS repository contains a merge from the Linux 2.4.23 kernel, but it is untested for single processor, and incomplete for SMP. We recommend that you use the 2.4.22 branch from CVS, which is accessed with the tag linux_2_4_22.

To configure the L4Linux kernel, follow the same basic steps used to configure a normal Linux kernel. Due to some virtualization of the platform, you may need to experiment with options to see whether they cause the behavior intended.

For the configuration submenu "L4Linux options", you must select "L4/X.2" for the "L4 kernel version". And you must set the path to the L4 user directory, for example /home/yoda/pistachio/user. When compiling for single processor, you may or may not choose the "tamed" option.

When using a ramdisk, be weary of its size. The default Linux ramdisk driver creates multiple ramdisk devices. And thus if you use a 64MB ramdisk, Linux may attempt to allocate four 64MB ramdisks. Currently, Linux requires that you manually modify the source code in linux/drivers/block/rd.c to set the number of ramdisk devices. In that file, adjust the NUM_RAMDISKS constant to 1.

After configuring the Linux kernel, build the dependencies with make dep. Then build the kernel with make. If successful, it produces an L4Ka::Pistachio compatible binary named vmlinuz.VX2.

Known Bugs and Issues

debug: L4Linux still contains plenty of debug code which will produce output under normal and abnormal conditions. It also contains plenty of opportunities for entering the L4Ka::Pistachio kernel debugger, in which case L4Linux ceases to run on the CPU which entered the kernel debugger. Debug output may be printed via printk() or herc_printf(). The herc_printf() function is tied directly to the L4 kernel debugger. During initialization of L4Linux, printk() output is buffered, and won't be dumped until Linux is sure that the console is initialized. But the herc_printf() output is unbuffered, and thus visible immediately via the L4 kernel debugger.
/dev/console: L4Linux has an incomplete, default console device. After the kernel boots, and prior to starting /sbin/init, the kernel may report that it is unable to open an initial console. When unable to open an initial console, /dev/console becomes an invalid device. You can avoid this problem by telling L4Linux to enable specific consoles, via command line parameters on its boot command line. You can also use multiple consoles and thus use the L4 debug console (called herc) along with standard Linux consoles. The last console specified on the command line is used for /dev/console. But all specified consoles receive kernel output. For example, to activate the L4 debug console (which could be the first serial port), and the second serial port as the official /dev/console, then use the command line parameters console=herc console=ttyS1,115200. Or to activate the L4 debug console, along with the tty device (such as VGA) for /dev/console, then use the command line parameters console=herc console=tty.
Memory for L4Ka::Pistachio: L4Ka::Pistachio currently lacks dynamic memory growth. It thus must be booted with sufficient memory resources to allocate page tables for all L4Linux user applications. The initial memory for L4Ka::Pistachio is provided by the L4Ka::Kickstart utility. The amount of initial memory is a compile-time constant in the L4Ka::Kickstart utility. To adjust, change the ADDITIONAL_KMEM_SIZE constant in the file pistachio/user/util/kickstart/ia32.cc.
Linux modules: L4Linux is unable to compile/build when module version numbers are enabled. Thus disable CONFIG_MODVERSIONS.
Virtual processors: L4Linux will start as many virtual processors as specified by the maxcpus kernel parameter. The virtual processors are distributed round robin on the physical processors, starting with CPU zero. If the number of virtual processors exceeds the number of physical processors, L4Linux will eventually deadlock due to priority inversion of the interrupt thread to the kernel thread of another virtual CPU on the same physical processor.
Signal Handling: There is a race condition for signal delivery to a freshly starting application.
Threads: Currently (and this must be fixed!) every Linux thread within a Linux process has a dedicated address space. Thus thread switching involves address space switching, where previously unexpected. The per-thread address spaces share the exact same mappings; the address spaces are thus transparent, and the behavior is as if they didn't exist, other than for the additional burden on Linux thread switch costs, and waste of L4 kernel memory.

Reporting Problems

L4Linux is a complicated system. Users can configure it with many options, most of which we can not duplicate. Thus when reporting problems, include an extensive description of the symptoms, an analysis, and description of the configuration. Simple bug reports which lack detailed information will likely be ignored.

Mandatory information: L4 microkernel name (e.g. is it L4Ka::Pistachio or Fiasco?), and the microkernel version (or is it from CVS, and if so, on what day?), and the compiler versions used for L4Ka::Pistachio and for L4Linux.

Capturing Debug Output

Often a problem will manifest as an unhandled exception, with information dumped to the L4Ka::Pistachio kernel debugger console and/or the Linux kernel console, accompanied by invocation of the kernel debugger. You should include any information printed with these bug messages. And often the messages will contain addresses. The addresses usually must be interpreted by you, and thus you must determine the faulting process, and map the faulting address to a function in that process. This is only necessary for bugs within sigma0 and L4Linux; Linux user applications will not cause problems, unless it is within the emulib mapped into every Linux user application. You can map addresses to function names by analyzing the vmlinux binary produced from an L4Linux build.

We highly recommend that you use a serial port for the L4Ka::Pistachio kernel debugger output. Using the serial console facilitates debug, especially if the VGA console is in graphics mode. VMware supports a serial console.

Trouble Shooting

You updated L4Ka::Pistachio and it didn't have an effect.: Remember that L4Linux is configured to access a specific L4Ka::Pistachio source directory, to obtain user-level header files. If you have a new L4Ka::Pistachio in a different location, then update your L4Linux configuration. Also remember to update your GRUB menu.lst file to point at new versions of binaries.
You updated L4Linux and it didn't have an effect.: If you changed L4Linux but loaded the old version, ensure that you successfully built the new version (sometimes the Linux build scripts hide errors, especially for parallel builds). Linux has severe problems with its dependency analysis, so it may not detect changes in source files, in which case you can touch the files or execute make clean. Also confirm that your GRUB menu.lst file points at the new version.

Decomposing

It is often possible to determine the faulting process by inspection of the faulting address. The readelf utility can be used to determine the link addresses of the various binaries. Typically, L4Ka::Pistachio/ia32 will use addresses above 0xF0100000, sigma0 will use addresses between 0x00020000 and 0x00030000, and L4Linux will use addresses between 0x003FF000 and 0x00700000. L4Linux user-level applications are dynamically linked against a support library (named emulib), and typically uses the address region 0xA0008000 to 0xA0009000, mapped with read-only and execute privileges.

With the L4Ka::Pistachio kernel debugger, you can determine the class of a thread based on the thread's priority levels. The priority levels are described in l4linux/include/asm-l4/api-i386-VX2/config.h. Of interest are PRIO_IRQ, PRIO_PAGER, PRIO_SMP_NOTIFY, PRIO_KERNEL, and PRIO_USER_PROCESS.


	Mail to webmaster	© 2000-2008 University of Karlsruhe