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
Past
Publications
2009
|
 |
Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser
Dingo: Taming device drivers
Proceedings of the 4th EuroSys Conference, Nuremberg, Germany, April, 2009 |
|
|
|
Gernot Heiser
Hypervisors for consumer electronics
Proceedings of the 6th IEEE Consumer Communications and Networking Conference, Las Vegas, NV, USA, January, 2009 |
2008
|
|
|
André Hergenhan and Gernot Heiser
Operating systems technology for converged ECUs
6th Embedded Security in Cars Conference (escar), Hamburg, Germany, November, 2008 |
|
|
|
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! |
|
|
|
Gernot Heiser
The role of virtualization in embedded systems
1st Workshop on Isolation and Integration in Embedded Systems, Glasgow, UK, April, 2008 |
|
|
|
Gernot Heiser
Do microkernels suck?
9th Linux.Conf.Au, Melbourne, January, 2008 |
2007
|
|
|
Gernot Heiser
Your system is secure? Prove it!
USENIX ;login:, 32(6), 35–38, (December, 2007) |
|
|
|
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, Pisa, Italy, July, 2007
Preliminary version |
|
|
|
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) |
|
|
 |
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 |
|
|
|
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 |
|
|
|
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, 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, 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, Dresden, Germany, July, 2006 |
|
|
|
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
|
|
|
Gernot Heiser
Secure embedded systems need microkernels
USENIX ;login:, 30(6), 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, 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, Germany, November, 2005 |
|
|
|
Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur
Are virtual-machine monitors microkernels done right?
Technical Report PA005103, NICTA, October, 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, 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, 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
Proceedings of the 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, Sydney, Australia, October, 2004 |
|
|
|
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 |
|
|
|
Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, 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 |
|
|
|
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 |
|
|
 |
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 |
|
|
|
Cristan 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 Australasian Computer Systems Architecture Conference, Gold Coast, Australia, January, 2001 |
2000
|
|
|
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
|
|
|
Kevin Elphinstone
Virtual memory in a 64-bit microkernel, PhD Thesis, University of NSW, Sydney 2052, Australia, 1999
|
|
|
|
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
|
|
|
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, 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, Cape May, NJ, USA, May, 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 |
