Software
ERTOS (and its UNSW-based predecessor DiSy) has developed a number of software packages that are released as open source. This includes operating system (OS) kernels, OS personalities for microkernels, and OS ports and development tools.
These pages are a starting point for downloading the various packages and systems. General information about these packages and systems can be found in our Research pages. We recommend that first-time visitors check out our newcomers page to get an idea of what to expect from our software.
seL4
The seL4 microkernel currently is the world's only general-purpose OS kernel with a mathematical, machine-checked proof of functional correctness. We provide binaries of seL4 for different platforms (ARM11 and x86), the formal specification in human and machine-readable form, user-level sample code, and a para-virtualized Linux for seL4/x86.
L4
L4 forms the base of most of our work. It is a state-of-the-art, high-performance microkernel. Our version, NICTA::Pistachio-embedded, now forms the basis of OKL4 3.0, developed by Open Kernel Labs. OKL4 is specifically aimed at the requirements of embedded systems, in particular small size and high performance.
Download the latest version of OKL4 from okl4.org. You may also be interested in our port to the HTC Dream (also known as the G1), available here.
We have ported part of the Android runtime (the Dalvik virtual machine and portions of the system server) to OKL4. This port is available here.
CAmkES
CAmkES is a component-based software development framework for L4. It provides a framework and environment that significantly simplifies development of complete multiserver systems on L4.
In CAmkES a system is modelled as a set of interacting software components. These software components have explicit interaction interfaces and a system design that explicitly details the connections between the components.
The development framework provides: a language to describe component interfaces, components, and whole component-based systems; a tool that processes these descriptions to combine programmer-provided component code with generated scaffolding and glue code to build a complete, bootable, system image; and full integration in the OKL4 environment and build system.
Find more details and download it from the CAmkES pages.
vNUMA
vNUMA is a virtual machine environment that turns a cluster of Itanium machines into a single NUMA system, albeit with some performance penalty.
Find more details from the vNUMA research page; you can download a snapshot from the vNUMA software page.
Linux-on-Linux
An offshoot of the vNUMA project, Linux-On-Linux is a User-mode Linux workalike for IA64.
Find more details and download it from the Virtualisation pages.
Fast Address-Space Switching
ARM7 and ARM9 cores feature virtually-addressed caches and TLBs not tagged with an address-space identifier. As a consequence, most operating systems flush the caches and TLB on every context switch, which bears a very high cost.
Fast address-space switching is a technique which minimises cache flushes, and can result in reduction of context-switching costs by orders of magnitude. This technique is implemented in NICTA::Pistachio-embedded. For Linux, the patches have been integrated into Secure Computing's Secure Snapgear firewall.
Sulima
Sulima is an instruction-set-architecture simulator for the MIPS64 architecture. It was developed at UNSW by Patryk Zadarnowski and has since been maintained at ERTOS. It specifically supports the U4600 platform (based on an R4700 processor) which we use for most MIPS-based development. It is also used for teaching at UNSW.
The latest version of Sulima is available for download.
Benchmarks
Performance evaluation and tuning is an inherent part of our work, and often no suitable standard benchmarks are available. People then tend to develop ad-hoc benchmarks, some of which develop into generally useful tools.
We offer some of our better-developed benchmark suites for download.
Related software includes a tool for recording and replaying (3 KiB) input events on Linux systems. This tool simplifies and improves repeatability of benchmarks requiring user input.
Demonstrators
We offer a simple VOIP system built on OKL4 as a demonstrator of building systems on L4. This was the result of student work, and besides being used as a demo for several events, was also used as an application scenario for some of our scheduling research.
We provide more information and the source code on a separate page.