University of Karlsruhe the University of New South Wales

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.

Internally we are now using OKL4 for projects that use the microkernel, such as component architectures and power management. It is also used for teaching the Advanced Operating Systems course at UNSW

People

Publications

2009

plain text PDF Joshua LeVasseur
Device-driver reuse via virtual machines, PhD Thesis, School of Computer Science and Engineering, Sydney, Australia, 2009
plain text PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser
Dingo: Taming device drivers
Proceedings of the 4th EuroSys Conference, Nuremberg, Germany, April, 2009
plain text PDF Gernot Heiser
Hypervisors for consumer electronics
Proceedings of the 6th IEEE Consumer Communications and Networking Conference, Las Vegas, NV, USA, January, 2009

2008

plain text PDF André Hergenhan and Gernot Heiser
Operating systems technology for converged ECUs
6th Embedded Security in Cars Conference (escar), Hamburg, Germany, November, 2008
plain text PDF Joshua LeVasseur, Volkmar Uhlig, Yaowei Yang, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser
Pre-virtualization: Soft layering for virtual machines
Proceedings of the 13th IEEE Asia-Pacific Computer Systems Architecture Conference, Hsinchu, Taiwan, August, 2008
Best Paper Award!
plain text PDF Gernot Heiser
The role of virtualization in embedded systems
1st Workshop on Isolation and Integration in Embedded Systems, Glasgow, UK, April, 2008
plain text   Gernot Heiser
Do microkernels suck?
, January, 2008

2007

plain text PDF Gernot Heiser
Your system is secure? Prove it!
USENIX ;login:, 32(6), 35–38, (December, 2007)
plain text PDF Kevin Elphinstone, David Greenaway and Sergio Ruocco
Lazy scheduling and direct process switch — merit or myths?
Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Pisa, Italy, July, 2007
Preliminary version
plain text PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, 41(4), 3–11, (July, 2007)
plain text link 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, 80(5), 687–699, (May, 2007)
Preprint
plain text PDF Timothy Roscoe, Kevin Elphinstone and Gernot Heiser
Hype and virtue
Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007
plain text PDF Carl van Schaik and Gernot Heiser
High-performance microkernels and virtualisation on ARM and segmented architectures
Proceedings of the 1st International Workshop on Microkernels for Embedded Systems (MIKES), Sydney, Australia, January, 2007

2006

plain text PDF 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
plain text 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
plain text PDF Sergio Ruocco
Real-Time Programming and L4 Microkernels
Proceedings of the 2nd Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Dresden, Germany, July, 2006
plain text PDF Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur
Are virtual-machine monitors microkernels done right?
ACM Operating Systems Review, 40(1), 95–99, (January, 2006)

2005

plain text PDF Gernot Heiser
Secure embedded systems need microkernels
USENIX ;login:, 30(6), 9–13, (December, 2005)
plain text PDF 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, Montego Bay, Jamaica, December, 2005
plain text PDF Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco
L4cars
3rd Embedded Security in Cars Conference (escar), Cologne, Germany, November, 2005
plain text PDF Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur
Are virtual-machine monitors microkernels done right?
Technical Report PA005103, NICTA, October, 2005
plain text PDF 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
plain text PDF Harvey Tuch, Gerwin Klein and Gernot Heiser
OS verification — now!
Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Santa Fe, NM, USA, June, 2005
plain text PDF 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, Anaheim, CA, USA, April, 2005
Best Student Paper Award!
plain text PDF Ben Leslie, Carl van Schaik and Gernot Heiser
Wombat: A portable user-mode Linux for embedded systems
6th Linux.conf.au, Canberra, April, 2005
plain text PDF 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

plain text PDF 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
plain text PDF Harvey Tuch and Gerwin Klein
Verifying the L4 virtual memory subsystem
Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004
plain text PDF Kevin Elphinstone and Stefan Goetz
Initial evaluation of a user-level device driver framework
Proceedings of the 9th Asia-Pacific Computer Systems Architecture Conference, Beijing, China, September, 2004
plain text PDF Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, Park City, Utah, USA, September, 2004
plain text PDF Ihor Kuz
L4 user manual — API version X.2
June, 2004

2003

plain text PDF 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
plain text PDF Christan Szmajda and Gernot Heiser
Generalised radix page table: A page table for modern architectures
Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003
plain text PS 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

plain text PDF Shane Stephens and Gernot Heiser
Fault tolerance and avoidance in biomedical systems
Proceedings of the 10th SIGOPS European Workshop, St Emilion, France, September, 2002
plain text PDF 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
plain text PDF 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

plain text PDF Gernot Heiser
Dealing with TLB tags
2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001
plain text PS Cristan Szmajda
Calypso: A portable translation layer
2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001
plain text PDF 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
plain text PS Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller
The SawMill framework for VM diversity
Proceedings of the 6th Australasian Computer Systems Architecture Conference, Gold Coast, Australia, January, 2001

2000

plain text PDF Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin J. Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther
The Sawmill multiserver approach
Proceedings of the 9th SIGOPS European Workshop, Kolding, Denmark, 2000

1999

plain text PS Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual: MIPS R4x00, version 1.11, kernel version 79
Sydney, Australia, May, 1999
plain text PS Kevin Elphinstone
Virtual memory in a 64-bit microkernel, PhD Thesis, School of Computer Science and Engineering, Sydney, Australia, 1999
plain text PDF 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, Rio Rico, AZ, USA, March, 1999
plain text PS Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
Page tables for 64-bit computer systems
Proceedings of the 4th Australasian Computer Architecture Conference, Auckland, New Zealand, January, 1999

1998

plain text PDF 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
plain text PDF 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

plain text PDF 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
plain text PDF 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, Cape Cod, MA, USA, May, 1997

1996

plain text PS 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), Cape May, NJ, USA, May, 1996
plain text PDF Jochen Liedtke and Kevin Elphinstone
Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization
ACM Operating Systems Review, 30(1), 4–15, (January, 1996)

1995

plain text PDF 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