Gernot Heiser | |
|---|---|
 Gernot Heiser speaking at the UNSW CSE Research Expo October 25 2022 | |
| Born | 1957 (age 68–69) |
| Education | University of Freiburg, BSc Brock University, MSc ETH Zurich, PhD |
| Known for | Operating system teaching, research, commercialising |
| Awards | Leopoldina Member (2023) RSN Fellow (2022) ACM SIGOPS Hall of Fame Award (2019) ATSE Fellow (2016) IEEE Fellow (2016) ACM Fellow (2014) |
| Scientific career | |
| Fields | Computer science |
| Institutions | University of New South Wales (ScientiaProfessor andJohn Lions Chair of Operating Systems) NICTA (research group leader) Open Kernel Labs (founder, former CTO, director) |
| Website | gernot-heiser |
Gernot Heiser (born 1957) is a German-Australian computer scientist. He is a ScientiaProfessor and theJohn Lions Chair foroperating systems atUNSW Sydney, where he leads theTrustworthy Systems group (TS).
Heiser earned hisAbitur in 1976 at the Markgräfler Gymnasium Müllheim inMüllheim im Markgräflerland.[1]
In 1991, Heiser joined theSchool of Computer Science and Engineering ofUNSW Sydney, originally as a lecturer, reaching the rank of full professor in 2002, a position he retains to date.
Also in 2002 he joined the newly created research organisationNICTA as one of its initial Program Leaders, in charge of the Embedded, Real-Time and Operating Systems (ERTOS) program. After a re-organisation in 2011 ERTOS became the Software Systems Research Group (SSRG) which he led. When NICTA was absorbed intoCSIRO in 2016, Heiser stepped back from management of the group, which was then called Trustworthy Systems (TS). In 2021 CSIRO abandoned TS,[2] at which time Heiser took the group back to UNSW and re-assumed its leadership.
Since April 2020, Heiser serves as the Founding Chairman of theseL4 Foundation.
Heiser's research focuses onmicrokernels, microkernel-based systems, andvirtual machines, and emphasizes performance and reliability.
His group producedMungi, asingle address space operating system,[3]for clusters of64-bit computers, and implementations of theL4 microkernel with very fastinter-process communication.[4]His Gelato@UNSW team was a founding member of theGelato Federation, and focused on performance and scalability ofLinux onItanium. They established theoretical and practical performance limits ofmessage passinginter-process communication (IPC) on Itanium.[5]
After joining NICTA at its creation in 2002, his research shifted away from high-end computing platforms, and toward embedded systems, with the aim of improving security, safety, and reliability via use of microkernel technology.[6]This led to the development of a new microkernel, called seL4, and its formal verification, claimed to be the first-ever complete proof of the functional correctness of a general-purpose OSkernel.[7]
His work on virtualization was motivated by the need to provide a complete OS environment on his microkernels. His Wombat project followed the approach taken with the L4Linux project atDresden, but was a multi-architectureparavirtualized Linux running onx86,ARM andMIPS hardware. The Wombat work later formed the basis for the OKL4hypervisor of his companyOpen Kernel Labs (OK Labs).The desire to reduce the engineering effort of paravirtualization led to the development of thesoft layering approach of automated paravirtulization which was demonstrated onx86 andItanium hardware.[8]His work on virtual non-uniform memory access (vNUMA) demonstrated a hypervisor which presents a distributed system as a shared-memory multiprocessor as a possible model for many-core chips with large numbers of processor cores.[9]
Device drivers are another focus of his work, including the first demonstration of user-mode drivers with a performance overhead of less than 10%,[10]an approach to driver development that eliminates most typical driver bugs by design,[11]device drivers produced from device test benches,[12]and a demonstration of the feasibility of generating device drivers automatically from formal specifications.[13]He also conducted research on operating-system-level energy management.[14]
Since leaving OK Labs in 2010 he focussed almost exclusively on seL4 and high-assurance seL4-based systems, both in research and in technology transfer. Notable research achievements include sound and completeworst-case execution-time (WCET) analysis of seL4, claimed to be the first ever such analysis for aprotected-mode OS kernel.[15][16]His work on extending seL4’s functionality to supportmixed-criticality systems (MCS) led to making time a first-class resource in seL4’scapability system.[17]
Focussing onmicroarchitecturaltiming channels, he demonstrated in 2015 the first practical cross-core timing side channel attack.[18]This led to work on the systematic prevention of timing-channel leakage, and the proposal of a set of mechanisms for achieving this, collectively referred astime protection.[19]
In the past, he also worked onsemiconductor devicesimulation, where he pioneered use of multi-dimensional modeling to optimizesilicon-basedsolar cells.[20]
| Kernels |
| ||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Operating systems |
| ||||||||||||||||||||||||
| Frameworks,kits | |||||||||||||||||||||||||
| Developers | |||||||||||||||||||||||||
| |||||||||||||||||||||||||
