Our Partners
The L4 Microkernel
The L4 microkernel provides a minimal and efficient basis for constructing operating system software for a broad range of systems from single-purpose embedded devices to multi-processor servers.
Prior to the commencement of the seL4 project, most of our L4 activities were based on L4Ka::Pistachio from the Karlsruhe L4KA Team. We have contributed and were maintaining the ARM, MIPS, Alpha and PowerPC-64 ports, and have dramatically improved the performance of the Itanium port.
The design and implementation of L4Ka::Pistachio are influenced by the desire to achieve a scalable, high-performance platform for desktop and server use. This implied a number of design decisions which make the kernel suboptimal for embedded use. We have therefore created a new specification, called L4-embedded, and a corresponding implementation called NICTA::Pistachio-embedded.
Our embedded version of L4 was successfully commercialised, initially via direct engagement with QUALCOMM and other companies. This lead to spinning out our development team into the new company Open Kernel Labs (OK Labs). OK Labs has further developed L4-embedded into what is now called OKL4, and provides products and services based on this system.
Publications
2009
|
 |
Joshua LeVasseur Device-driver reuse via virtual machines PhD Thesis, UNSW, Sydney, Australia, May, 2009 |
2008
|
|
 |
Gernot Heiser Do microkernels suck? Other Conference Presentation, Linux.conf.au, Melbourne, Australia, January, 2008. |
2007
|
|
Gernot Heiser Virtualisation for embedded systems Technical Report, Open Kernel Labs, November, 2007 |
|
|
 |
Ihor Kuz, Yan Liu, Ian Gorton and Gernot Heiser CAmkES: A component model for secure microkernel-based embedded systems Journal of Systems and Software Special Edition on Component-Based Software Engineering of Trustworthy Embedded Systems, Volume 80, Number 5, pp. 687–699, May, 2007 Preprint |
|
|
|
Carl van Schaik and Gernot Heiser High-performance microkernels and virtualisation on ARM and segmented architectures International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007 |
2006
|
|
|
Sergio Ruocco User-level fine-grained adaptive real-time scheduling via temporal reflection Proceedings of the 27th IEEE Real-Time Systems Symposium, Rio De Janeiro, Brazil, December, 2006 |
|
|
|
Geoffrey Lee and Charles Gray L4/Darwin: Evolving UNIX Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Vic, Australia, October, 2006 Slides |
|
|
|
Sergio Ruocco Real-Time Programming and L4 Microkernels Proceedings of the 2nd Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Dresden, DE, July, 2006 |
|
|
|
Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur Are virtual-machine monitors microkernels done right? ACM Operating Systems Review, Volume 40, Number 1, pp. 95–99, January, 2006 |
2005
|
|
|
Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, Volume 30, Number 6, pp. 9–13, December, 2005 |
|
|
|
Harvey Tuch and Gerwin Klein A unified memory model for pointers Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 474–488, Montego Bay, Jamaica, December, 2005 |
|
|
|
Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco L4cars 3rd Embedded Security in Cars Conference (escar), Cologne, DE, November, 2005 |
|
|
|
Joshua LeVasseur, Volkmar Uhlig, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser Pre-virtualization: Slashing the cost of virtualization Technical Report PA005520, NICTA, October, 2005 |
|
|
|
Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Proceedings of the 10th Workshop on Hot Topics in Operating Systems (HotOS), pp. 7–12, Santa Fe, NM, USA, June, 2005 |
|
|
|
Charles Gray, Matthew Chapman, Peter Chubb, David Mosberger-Tang and Gernot Heiser Itanium — a system implementor's tale Proceedings of the 2005 USENIX Annual Technical Conference, pp. 264–278, Anaheim, CA, USA, April, 2005 Best Student Paper Award |
|
|
|
Ben Leslie, Carl van Schaik and Gernot Heiser Wombat: A portable user-mode Linux for embedded systems 6th Linux.conf.au, Canberra, April, 2005 |
|
|
|
Rafal Kolanski A formal model of the L4 micro-kernel API using the B method Technical Report Technical Report 05-00029-1, National ICT Australia, 2005 |
2004
|
|
|
Kevin Elphinstone Future directions in the evolution of the L4 microkernel Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004 |
|
|
|
Harvey Tuch and Gerwin Klein Verifying the L4 virtual memory subsystem Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, pp. 73–97, Sydney, Australia, October, 2004 |
|
|
|
Kevin Elphinstone and Stefan Götz Initial evaluation of a user-level device driver framework Proceedings of the 9th Asia-Pacific Computer Systems Architecture Conference, Beijing, China, September, 2004 |
|
|
|
Gerwin Klein and Harvey Tuch Towards verified virtual memory in L4 TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004 |
|
|
|
Ihor Kuz L4 user manual — API version X.2 June, 2004 |
2003
|
|
|
Andreas Haeberlen and Kevin Elphinstone User-level management of kernel memory Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003 |
|
|
|
Chris Szmajda and Gernot Heiser Generalised radix page table: A page table for modern architectures Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, pp. 290-304, Aizu-Wakamatsu City, Japan, September, 2003 |
|
|
|
Adam Wiggins, Harvey Tuch, Volkmar Uhlig and Gernot Heiser Implementation of fast address-space switching and TLB sharing on the StrongARM processor Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003 |
2002
|
|
|
Shane Stephens and Gernot Heiser Fault tolerance and avoidance in biomedical systems Proceedings of the 10th SIGOPS European Workshop, St Emilion, France, September, 2002 |
|
|
|
Daniel Potts, Simon Winwood and Gernot Heiser Design and implementation of the L4 microkernel for Alpha multiprocessors Technical Report UNSW-CSE-TR-0201, School of Computer Science and Engineering, February, 2002 |
|
|
|
Volkmar Uhlig, Uwe Dannowski, Espen Skoglund, Andreas Haeberlen and Gernot Heiser Performance of address-space multiplexing on the Pentium Technical Report 2002-1, Computer Science Department, University of Karlsruhe, 2002 |
2001
|
|
|
Gernot Heiser Dealing with TLB tags 2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001 |
|
|
|
Chris Szmajda Calypso: A portable translation layer 2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001 |
|
|
|
Daniel Potts, Simon Winwood and Gernot Heiser L4 reference manual: Alpha 21x64 Technical Report UNSW-CSE-TR-0104, School of Computer Science and Engineering, March, 2001 |
|
|
|
Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller The SawMill framework for VM diversity Proceedings of the 6th Asia-Pacific Computer Systems Architecture Conference, pp. 3–10, Gold Coast, Australia, January, 2001 |
1999
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual: MIPS R4x00, version 1.11, kernel version 79 Sydney, Australia, May, 1999 |
|
|
|
Kevin Elphinstone Virtual memory in a 64-bit microkernel PhD Thesis, UNSW, Sydney, Australia, March, 1999 |
|
|
|
Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko and Yoonho Park Flexible access control using IPC redirection Proceedings of the 7th Workshop on Hot Topics in Operating Systems (HotOS), pp. 191–196, Rio Rico, AZ, USA, March, 1999 |
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Proceedings of the 4th Australasian Computer Architecture Conference, pp. 211-226, Auckland, New Zealand, January, 1999 |
1998
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Technical Report UNSW-CSE-TR-9804, School of Computer Science and Engineering, August, 1998 |
|
|
|
Alan Au and Gernot Heiser L4 User Manual — version 1.0 Technical Report UNSW-CSE-TR-9801, School of Computer Science and Engineering, April, 1998 |
1997
|
|
|
Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual – MIPS R4x00 — Version 1.0 Technical Report UNSW-CSE-TR-9709, School of Computer Science and Engineering, December, 1997 |
|
|
|
Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Herrman Härtig, Gernot Heiser, Nayeem Islam and Trent Jaeger Achieved IPC performance (still the foundation for extensibility) Proceedings of the 6th Workshop on Hot Topics in Operating Systems (HotOS), pp. 28–31, Cape Cod, MA, USA, May, 1997 |
1996
|
|
|
Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke Supporting persistent object systems in a single address space Proceedings of the 7th International Workshop on Persistent Object Systems (POS), pp. 111–119, Cape May, NJ, USA, May, 1996 |
|
|
|
Jochen Liedtke and Kevin Elphinstone Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization ACM Operating Systems Review, Volume 30, Number 1, pp. 4–15, January, 1996 |
1995
|
|
|
Jochen Liedtke and Kevin Elphinstone Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization Technical Report UNSW-CSE-TR-9503, School of Computer Science and Engineering, November, 1995 |