L4Ka::Pistachio/x86-x32

The x86-x32 (IA32) port of L4Ka::Pistachio is the reference architecture and therefore in the most complete state. It supports most features of the Version 4 API and has relatively.

Features

• SMP support
• Support for hardware-assisted processor virtualization on Intel Processors (VT-x)
• Optimized IPC fast path

Supported Hardware

L4Ka::Pistachio/x86-x32 was tested on a wide variety of system configurations. The following system configurations are supported and known to work:

• Intel i486
• Intel Pentium, Pentium II, Pentium IV, Core
• AMD K9, K10
• VMware Workstation, Qemu, Simics

Multi-processors and APIC/IOAPIC support require a system with ACPI. Older MP systems only providing Intel's MP structure are not supported and can therefore only be used in PIC and uniprocessor mode. L4Ka::Pistachio/x86-x32 was tested on the following multi-processor systems:

• 8-way K10 with 4GB RAM
• 8-way Pentium 4 HT 2.2GHz with 1MB L3 cache, 8GB RAM
• 4-way Pentium 3 Xeon 700MHz with 1MB L2 cache, 1.25GB RAM
• 2-way Pentium 3 800MHz, 256K L2 cache, 768MB RAM

All listed performance measurements were conducted on the dual P3 system.

Building and Booting

Step-by-step instructions for building L4Ka::Pistachio/x86-x32 can be found in Getting Started with L4Ka::Pistachio on x86-x32.

We perform unattended weekly builds of L4Ka::Pistachio. Check the result of the last run.

Kernel

The kernel can be built using GCC 2.95.2 and higher. However, we highly recommend using GCC 3.2 or newer to make use of the far better code optimizations and thereby getting better performance results. Since most development systems are x86-x32 we assume that cross compilation is a non-issue.

The kernel debugger can direct its I/O via the serial line or the keyboard/screen. Be sure to configure your kernel for the appropriate I/O device.

User-Level

The user-level applications are configured to use the serial port for I/O by default. To use screen I/O, run the configure script with the --without-comport command line option.

If you want to use the serial port, you can choose a particular port by either specifying an index (0, 1, 2, or 3), or its physical device address (e.g. 0x3f8), with the --with-comport= command line option.

Booting

The kernel can be booted using GRUB and L4Ka::KickStart; latter is part of the kernel distribution. GRUB requires a configuration file which contains all modules to be loaded. Besides the kernel image itself further modules can be loaded. The kernel requires at least sigma0 and the root task. Following an example menu.lst file:

GRUB supports network booting using the TFTP protocol. For more details refer to the corresponding documentations. A ready-to-run GRUB floppy image can be generated and downloaded fromhere.

After booting, GRUB starts L4Ka::KickStart which then configures the kernel configuration page using the boot-loader provided configuration information. Afterwards, L4Ka::Kickstart hands over control to the kernel which bootstraps sigma0, sigma1 (if available), and the root task.

Runtime Output

The kernel prints diagnostic information to the screen (if the kernel debugger is enabled). The information appears as "spinning" characters in the upper right corner, one row per processor. The character will change upon kernel events. The events, in reverse display order (right to left), are:

• idler invocation
• timer interrupt
• hardware interrupts
• end-of-timeslice
• cross-processor

If the kernel prints the message "KD# System started (press 'g' to continue)" at startup and does not continue booting, and you don't know why, simply press 'g' to continue. This feature allows to set breakpoints and the like before the first user threads are executed. You can control this behavior with the option "Enter kernel debugger on startup" in the Debugger menu of the kernel configuration utility.

If the kernel prints the error message "CPU does not support all features (XYZ) -- halting" then the processor does not support required features to operate the kernel. XYZ represents a feature mask, which is validated against the CPUID instruction. When the kernel is configured for verbose init, it will print cryptic strings representing the missing features (the cryptic strings correlate to features enumerated in the x86-x32 manuals). To solve the problem, configure the kernel to use an older generation processor.

Missing Features / Known Bugs

• Lipc not implemented
• IPC does not return local thread IDs on intra-address space IPC
• Kernel crashes without warning on systems not supporting 4MB pages
• A post-Pentium kernel crashes without warning on Pentium systems
• Kernel-ptab synchronization has race on SMP systems
• SMP support for pre-ACPI systems missing