Trustworthy Systems

Virtualization

Virtual machines are important not only in the enterprise domain, but also in embedded systems. The main reasons are their ability to support legacy re-use, and to provide a convenient environment in an otherwise bare-bones system. For example, a complete Linux system can be provided as a convenient high-level programming environment for application programs and sophisticated user interfaces. Virtualization supports such an environment while at the same time isolating the safety- or security-critical components or real-time subsystems from interference.

Furthermore, in multi- and many-core systems-on-chip, the indirection provided by virtualization is becoming be essential for effective management of global system resources, in particular energy.

Rather than being a primary research topic, virtualization for us is a vehicle for building complete systems on top of the seL4 microkernel (acting as a hypervisor), and an instance of a security architecture. Virtualization is an essential mechanism for our work on multi-criticality real-time systems.

Current Activities

Present activities focus two issues:

Much of this work is not virtualization research of its own right, but instead is research that is heavily dependent on virtualization as a mechanism, and drives performance improvements.

Past activities

RapiLog: Reducing system complexity and improving performance by leveraging hypervisor dependability

Performance gains with RapiLog

We usually think of a high-assurance system like seL4 as an enabler for security- or safety-critical systems. However, we can leverage its dependability guarantees in circumstances where people nowadays go to great lengths to ensure dependability at the expense of increased complexity and often reduced performance.

RapiLog is a demonstration that things can be both simpler and faster when using seL4: It can boost database throughput by up to 100% (see figure on the right), with a simpler setup that leverages virtualization.

RapiLog system architecture

We run an unmodified database system on an unmodified (except for a custom driver) Linux system in a virtual machine on top of seL4. A virtual disk safely buffers log data and writes it to disk asynchronously, yet guarantees that the log is recoverable, even in the case of crashes of Linux or the DBMS, or of power blackouts. More details in the RapiLog paper (below).

 

Wombat and Darbat

Wombat was our para-virtualized Linux server on L4. It was the first portable (across architectures) version of a virtualized Linux on L4 (possibly the first portable virtualized Linux at all). It was later commercially supported by our spinout company Open Kernel Labs under the name OK Linux. We have consequently discontinued support for Wombat.

Darbat is a related project aiming at running a complete Mac OS X system on top of L4, possibly concurrently with a Linux (i.e. Wombat) system. Rather than straight para-virtualization of the Darwin kernel (consisting of Mach, a BSD kernel and IOkit), the Darbat project attempted to remove Mach completely, replacing its functionality by plain L4 mechanisms plus some user-level libraries. The aim was to run Darwin and IOkit in different (unprivileged) address spaces.

Pre-virtualization

Pre-virtualization is a new virtualization technique, which dramatically reduces the engineering cost of para-virtualization while maintaining its performance advantage over pure virtualization. Pre-virtualization, like pure virtualization, retains the original host platform architecture. This is achieved by automating the process of virtualising the guest OS.

Itanium Hypervisors

Our pre-virtualization work supports several different hypervisors on the Itanium architecture. One of them (vNUMA) is our own research project, others are developed elsewhere.

vNUMA

Virtual NUMA (vNUMA) is a virtual machine monitor that provides a virtual shared-memory multiprocessor system on a cluster. It supports a pre-virtualised Linux as a single-system-image operating system. vNUMA aimed to provide easy and efficient migration of legacy SMP applications to a cluster.

Xen/ia64

Xen is a widely-used open-source hypervisor. We were targeting Xen for or pre-virtualised Linux and are achieving the same (or better) performance as para-virtualised XenoLinux, with a fraction of the engineering cost.

Linux

Linux itself, more commonly used as a guest OS, can serve as a hypervisor, user-mode Linux (UML) is an example of this. While UML is an example of para-virtualised Linux, our Linux-on-Linux achieves better performance with dramatically reduced engineering cost.

People

Current

Past

  • Adrian Danis
  • Aleksander Budzynowski
  • Alison Felizzi
  • Ben Leslie
  • Qian Ge
  • Siwei Zhuang

Publications

2022

Abstract
Slides
PDF
Presentation Video
Gernot Heiser, Lucy Parker, Ivan Velickovic, Peter Chubb and Ben Leslie
Can we put the "S" into IoT?
IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022

2020

Abstract PDF Gernot Heiser, Gerwin Klein and June Andronick
seL4 in Australia: From research to real-world trustworthy systems
Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020

2013

Abstract
Slides
PDF Gernot Heiser, Etienne Le Sueur, Adrian Danis, Aleksander Budzynowski, Tudor-Ioan Salomie and Gustavo Alonso
RapiLog: reducing system complexity through verification
EuroSys Conference, pp. 323–336, Prague, Czech Republic, April, 2013

2011

Abstract PDF Prashant Varanasi and Gernot Heiser
Hardware-supported virtualization on ARM
Asia-Pacific Workshop on Systems (APSys), pp. 5 pages, Shanghai, China, July, 2011
Abstract
Slides
PDF Gernot Heiser, Leonid Ryzhyk, Michael von Tessin and Aleksander Budzynowski
What if you could actually Trust your kernel?
Workshop on Hot Topics in Operating Systems (HotOS), pp. 1–5, Napa, CA, USA, May, 2011

2010

Abstract PDF Gernot Heiser and Ben Leslie
The OKL4 microvisor: Convergence point of microkernels and hypervisors
Asia-Pacific Workshop on Systems (APSys), pp. 19–24, New Delhi, India, August, 2010

2009

Abstract PDF Matthew Chapman and Gernot Heiser
vNUMA: A virtual shared-memory multiprocessor
USENIX Annual Technical Conference, pp. 349–362, San Diego, USA, June, 2009
Abstract PDF Joshua LeVasseur
Device-driver reuse via virtual machines
PhD Thesis, UNSW, Sydney, Australia, May, 2009
Abstract PDF Matthew Chapman
vNUMA: Virtual shared-memory multiprocessors
PhD Thesis, UNSW, Sydney, Australia, March, 2009
Abstract PDF Gernot Heiser
Many-core chips — a case for virtual shared memory
Workshop on Managed Many-Core Systems, pp. 4 pages, Washington, DC, USA, March, 2009
Abstract PDF Gernot Heiser
Hypervisors for consumer electronics
IEEE Consumer Communications and Networking Conference, pp. 1–5, Las Vegas, NV, USA, January, 2009

2008

Abstract PDF Joshua LeVasseur, Volkmar Uhlig, Yaowei Yang, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser
Pre-virtualization: Soft layering for virtual machines
Asia-Pacific Computer Systems Architecture Conference, pp. 1–9, Hsinchu, Taiwan, August, 2008
Best Paper Award
Abstract PDF
Presentation Video
Gernot Heiser
Do microkernels suck?
Other Conference Presentation, Linux.conf.au, Melbourne, Australia, January, 2008.

2007

plain text to be published Gernot Heiser
Virtualisation for embedded systems
Technical Report, Open Kernel Labs, November, 2007
Abstract PDF Timothy Roscoe, Kevin Elphinstone and Gernot Heiser
Hype and virtue
Workshop on Hot Topics in Operating Systems (HotOS), pp. 19–24, San Diego, USA, May, 2007
Abstract PDF Peter Chubb, Matthew Chapman and Myrto Zehnder
[para]virtualisation without pain
8th Linux.conf.au, Sydney, NSW, January, 2007
Abstract PDF 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

Abstract 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
Abstract PDF Myrto Zehnder and Peter Chubb
Virtualising PCI
Gelato ICE, Singapore, October, 2006
Abstract PDF 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

Abstract 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
Abstract PDF Matthew Chapman and Gernot Heiser
Implementing transparent shared memory on clusters using virtual machines
Proceedings of the 2005 USENIX Annual Technical Conference, pp. 383–386, Anaheim, CA, USA, April, 2005
Abstract 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, pp. 264–278, Anaheim, CA, USA, April, 2005
Best Student Paper Award
Abstract 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

2002

Abstract 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