L4 on MIPS R4x00

This Page is no longer Maintained!

What used to be UNSW's DiSy group is now part of the Embedded, Real-Time and Operating-Systems (ERTOS) Research Program at National ICT Australia (NICTA).

Up-to-date information on our L4 activities can be found at the ERTOS L4 site.

For general information on L4 refer to L4HQ.

Status

The R4x00 version of the L4 microkernel (L4/MIPS) used to be our main workhorse for research and teaching. It was developed at UNSW by then PhD student Kevin Elphinstone. The kernel consists of about 6,000 lines of assembler and 6,500 lines of C.

It is now superseded by our port of L4Ka::Pistachio to the MIPS64 architecture.

The kernel is stable since August 1997, with minor enhancements and bug fixes since. It has been tested on an R4600-based SGI Indy, on the Algorithmics P4000i prototyping board, as well as on the R4700-based U4600 system developed at UNSW as a research and teaching platform.

Documentation

The following documentation is available:

The L4/MIPS R4x00 Reference Manual
The L4 User Manual
UNIX manual pages describing the C interface to L4/MIPS
A rudimentary L4/MIPS FAQ
L4/MIPS Release Notes
A list of limitations and known bugs of the present release.
Inside L4/MIPS, annotated L4/MIPS source code.

Availability

L4/MIPS is available in source form under the terms of the GNU General Public License.