The Taub Faculty of Computer Science Events and Talks

Henry Taub Distinguished Visitor Lecture: The L4 microkernel has undergone 20 years of use and evolution. It has an active user and developer community, and there are commercial versions which are deployed on a large scale and in safety-critical systems. In this paper we examine the lessons learnt in those 20 years about microkernel design and implementation. We revisit the L4 design papers, and examine the evolution of design and implementation from the original L4 to the latest generation of L4 kernels, especially seL4, which has pushed the L4 model furthest and was the first OS kernel to undergo a complete formal verification of its implementation as well as a sound analysis of worst-case execution times. We demonstrate that while much has changed, the fundamental principles of minimality and high IPC performance remain the main drivers of design and implementation decisions.

Bio:
Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at the University of New South Wales (UNSW), and leads the Software Systems Research Group at NICTA, Australia's National Centre of Excellence for ICT Research. He joined NICTA at its creation in 2002, and before that was a full-time member of academic staff at UNSW from 1991. His past work included the Mungi single-address-space operating system (OS), several un-broken records in IPC performance, and the best-ever reported performance for user-level device drivers. More recently he led the team at NICTA which produced the world's first formal proof of functional correctness of a protected general-purpose operating-system kernel, the first published sound worst-case execution time analysis of a protected OS kernel, and the synthesis of high-performance device drivers.