L4Ka Project

L4Ka::Pistachio/x86-x64

L4Ka::Pistachio/x86-x64 supports AMD's 64bit extension to the x86-x32 instructions set (AKA X86-X64 and x86-x32e).

Features

  • SMP support
  • Compatibility mode (32-bit user applications)
  • Optimized IPC fast path

Supported Hardware

L4Ka::Pistachio/x86-x64 was tested with the following configurations:

  • AMD K9, K10 systems
  • Intel Pentium and Core Systems with EM64T extensions
  • VMware Workstation, Qemu, Simics

We conducted some performance measurements on a 1.6GHz AMD Opteron 242 system.

Building and Booting

Due to the similarities between the x86-x64 and x86-x32 versions we've been able to reuse most of the already existing infrastructure. Configuring and booting is almost identical to Pistachio/x86-x32. Kickstart will detect the 64bit version of the kernel and perform the respective configuration.

Kernel

The kernel can be built using GCC 3.3 and higher. 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. The binary distribution includes the kernel configurations for the respective kernel binaries.

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

User-Level

User-level binaries for x86-x64 are built by using the --host=x86-x64 switch. User-level applications are configured to use the serial port for I/O by default. To use other 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:

title=L4Ka::Pistachio
kernel=/kickstart
module=/x86-x64-kernel
module=/sigma0
module=/roottask

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 from here.

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 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 (mapped to IPC)