L4Ka::Pistachio/ARM

page maintained by Harvey Tuch (htuch@cse.unsw.edu.au)

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

Supported Hardware

• PLEB (Intel StrongARM SA-1100)
• Intel XScale IXP425
• TI OMAP1510 (ARM925T)

Porting to other ARM-based platforms should be fairly straight forward. The kernel should also run under the SkyEye simulator for the StrongARM using this configuration file.

This is the first public release of the kernel and so testing has been less extensive than on some of the other architectures. It is advised that users of this port check public CVS for the latest update.

Performance

The kernel features fast address-space switching (FASS) as a compile option. We have not subjected the kernel to large scale benchmarks, however we have experimental IPC times using a modified version of the supplied pingpong benchmark, optimised to take advantage of FASS, of approximately 330 cycles each way on inter-address space IPC, and 308 cycles on intra-address space IPC (measured on the PLEB with a 206.4 MHz clock frequency). The corresponding IPC times when FASS is disabled are 11218 and 239 cycles respectively. We anticipate that with the addition of fast-path IPC the inter-address space IPC time on FASS will be around 120-140 cycles. Even without this optimization, context-switching and IPC performance across address spaces, when FASS is used appropriately, improves on any existing ARM implementation of L4 by approximately two orders-of-magnitude.

Further information on FASS can be obtained from the following paper:

Building and Booting

We recommend using GCC 3.2 or above and the corresponding binutils to build the kernel and user applications.

To build a bootable kernel, follow the directions to configure and build the kernel, then configure and build the user applications. When this process has finished, the directory contrib/elf-loader/ will contain a binary image called arm-loader.bin.

Load this image into memory with the platform's bootloader and begin execution at the load address.

Missing Features and Known Bugs

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

• The kernel is missing the following optimizations (considered future work):
  • LIPC - Currently an LIPC system call takes the IPC path.
  • Fast-path IPC.
  • The performance when transferring StringItems through IPC is non-optimal.
• SMP is not supported.
• FPU support is missing.
• Exceptions other than SWI (documented in the reference manual under syscall emulation exception support) are not delivered to the user. Any exception which cannot be handled by the kernel causes the debugger to be invoked.