Trustworthy Systems

L4/Darwin (aka Darbat)

The L4/Darwin project was an experimental port of Darwin to the L4 microkernel to study the characteristics of a large-scale microkernel-based system. It includes a port of IOKit to L4, a modified libc to communicate with the Darbat Server, and of course XNU with many of the machine-dependent parts heavily modified (pmap, thread/task creation, etc) but much left unchanged (most of BSD, and large parts of OSFMK work without modification).

Current Plans

The aim was for Darbat to be fully binary compatible with existing userlevel Darwin binaries. There were also plans to integrate paravirtualised L4 Linux (Wombat) to run side-by-side with Darbat on the same machine and allow them to communicate via L4 IPC.

Given the amount of existing OS X code that depends on Mach, we are currently not aiming at completely removing Mach from Darwin. Instead we are modifying Darwin to make better use of L4 and profit from its performance. This includes:

Driver support

Driver support is provided by the IOKit. A range of drivers are supported, including PIIX ATA, USB (keyboard and mouse, USB stick), Intel 8255x ethernet, and generic serial. There is almost complete support for binary-loading of existing drivers.

Status

Supported Hardware

The following systems are supported through a FireWire based bootloader and debug console. Support for the builtin display and USB keyboard is available to use the shell.

While other systems may work, we haven't tested them yet.

Software support

Darbat boots into single user mode (launchd -s) and is able to run a range of commands including (but in no way limited to):

Things that still need to be implemented are:

There is full read/write support for the internal HD, and for testing purposes it is best to mount this drive and run commands directly from it. Currently 10.4.6 binaries found on release hardware will load successfully in Darbat.

Downloads

Darbat is available as both source and binaries. We are currently at Release 0.2. For more details and downloads, see the release page.

Conference Publications

Abstract PDF Geoffrey Lee and Charles Gray
L4/Darwin: Evolving UNIX
Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Vic, Australia, October, 2006
Slides

Theses

Abstract PDF Joshua Root
Virtualising Darwin on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, February, 2007
Abstract PDF Tom Birch
Performance limits of Darwin on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, October, 2006
Abstract PDF Geoffrey Lee
I/O kit drivers for L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2005
Abstract PS Ka-shu Wong
MacOS X on L4
BE Thesis, School of Computer Science and Engineering, Sydney, Australia, December, 2003