Virtualization
Virtual machines (what are they?) are of increasing importance in embedded systems, mostly for its ability to provide legacy re-use: For example, a complete Linux environment can be provided as a convenient high-level programming environment for application programs and sophisticated user interfaces. Virtualization support such an environment while at the same time isolating the safety- or security-critical components or real-time subsystems from interference.
In future multi- and many-core systems-on-chip, the indirection provided by virtualization will be essential for effective management of global system resources, in particular energy.
Consequently, virtualization for us is both a vehicle for building complete systems on top of the seL4 microkernel (acting as a hypervisor), an instance of a security architecture, and a research direction in its own right.
Below are examples of past virtualization research of the group, much of it in the context of the Gelato project.
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 is now commercially supported by our spinout company Open Kernel Labs under the name OK Linux. We have consequently discontinued support for Wombat.
Darbat is 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 attempts to remove Mach completely, replace its functionality by plain L4 mechanisms plus some user-level libraries. The aim is 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 projects, 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 aims to provide easy and efficient migration of legacy SMP applications to a cluster.
vNUMA will be released in the near future.
Xen/ia64
Xen is a widely-used open-source hypervisor. We are 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.
Our pre-virtualised Linux for Xen/ia64 will be released shortly.
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
Publications
2009
2008
2007
2006
|
 |
Geoffrey Lee and Charles Gray L4/Darwin: Evolving UNIX Conference for Unix, Linux and Open Source Professionals, Melbourne, Vic, Australia, October, 2006 Slides |
|
|
|
Myrto Zehnder and Peter Chubb Virtualising PCI Gelato ICE, Singapore, October, 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) |