Séminaire REGAL
The L4 Microkernel — from research to mass deployment and back
Mardi 29 juin 2010Gernot Heiser (NICTA)
This talk traces the journey of the L4 microkernel from its creation by Liedtke in the mid-'90s. L4 then was the first of the second-generation of microkernels, characterised by an order-of-magnitude improvement in message-passing performance over earlier microkernels. Adapted by the ERTOS group at NICTA for use in resource-constrained embedded systems, it was adopted for commercial deployment about 5 years ago and is now marketed by NICTA startup company Open Kernel Labs, with total shipments to date exceeding 750 million.
On-going research at NICTA has produced a third-generation microkernel called seL4, which has recently been formally proved to be functionally correct. SeL4 is now the basis of NICTA's research agenda towards truly trustworthy embedded systems. The talk will highlight some of these achievements, and discuss what we have learnt in 15 years of research and 5 years of commercial mass deployment.
Lamia.Benmouffok (at) nulllip6.fr