L4Ka Project
L4Ka Project
L4Ka Project
L4Ka Project
Pistachio
Pistachio/PowerPC32

L4Ka::Pistachio for PowerPC32

page maintained by Jan Stoess (stoes ∂does-not-exist.kit edu)

Welcome to the home of the L4Ka::Pistachio kernel for the PowerPC.

Features

  • SMP support
  • Support for full-virtualization

Supported Hardware

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

  • IBM PowerPC 440GP (tested on Simics AMCC Ebony Virtual Evaluation Board)
  • IBM PowerPC 450 (tested on the Blue Gene/P Supercomputer)

Older revisions of the kernel have been extensively tested on an Apple Pismo G3 PowerBook with IBM 750 500 MHz PowerPC. The kernel can principally configure the 750 processor and compatibles. However, in recent past, the focus has mainly been the embedded PowerPC versions thus kernel build an execution on 750 may not work correctly out of the box.

Building and Booting

Kernel and applications can be built using GCC 4.1 and newer. In our labs, we typically use cross compilers from speedblue or built via crosstool-ng.

Kernel

The kernel debugger can direct its I/O via the serial line or via Blue Gene’s collective tree network device. 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 the U-Boot embedded boot loader and L4Ka::KickStart; latter is part of the kernel distribution. For booting on Blue Gene, a special version of U-Boot is required, which is part of the Kittyhawk open-source project.

Performance

We have not subjected the PowerPC kernel to large scale benchmarks. But we have started to collect performance statistics related to kernel primitive operations. Available measures on the PowerPC 750: system call, IPC performance, and address space switch.

Missing Features and Known Bugs

The following are known issues with the PowerPC L4Ka::Pistachio kernel:

  • Performance problems related to the SVR4 ABI. A patch for gcc, which modifies the SVR4 ABI, has been developed internally but isn't ready for release.
  • SMP support is incomplete. The IPC fast path is incompatible with SMP. Access to the page hash is not SMP safe in all cases. And memory coherency may be incomplete. It works in the psim simulator, but race conditions could prevent its use under heavy workload.
  • Incomplete support for newer processors.
  • The format of the device tree passed from the boot loader to the kernel is undocumented.