L4Ka::Pistachio PowerPC Implementation (pdf) (ps): View our PowerPC L4Ka::Pistachio implementation overview, which offers techniques for optimizing performance on the PowerPC architecture.
Build and boot: Some detailed steps on building the kernel and user-level applications. Also includes hints on booting and running.
PowerPC Kernel Binary Interface: Information about the ABI used internally to the kernel.
l4hq.org: The L4 community site, l4hq.org, hosts more PowerPC documentation such as starting points for booting a custom kernel on Apple machines, and PowerPC development documentation.

Supported Hardware

The kernel has been extensively tested on an Apple Pismo G3 PowerBook with IBM 750 500 MHz PowerPC. The kernel can configure the 750 processor and compatibles. Newer processors, such as the 7455, will probably not be configured correctly.

The kernel can also execute under the psim PowerPC simulator. The simulator is distributed with the GNU gdb debugger, under gdb/sim/ppc. For psim build and configuration information, refer to the documentation included in the L4Ka::Pistachio source distribution: pistachio/doc/notes/ppc-build.txt.

Tested Hardware

We have limited access to PowerPC hardware. The following systems have been tested:

psim simulator	A patched simulator is necessary. Refer to PowerPC tool chain build instructions.
PowerPC 750 on the Pismo PowerBook (photo)	Complete support
PowerPC 7455 on the G4 1GHz PowerBook	The kernel boots and runs, but without full performance, and without a properly configured processor.

Warning: the kernel does not perform power management. The kernel is still under development. DO NOT leave your laptop running for long periods of time with the L4Ka::Pistachio kernel, unless you develop an appropriate power management device driver, or trust your firmware.

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.


	Mail to webmaster	© 2000-2008 University of Karlsruhe