From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels?

[Jim Huang]

hi all,

Kevin Elphinstone 與 Gernot Heiser 博士的最新論文，非常值得一讀：
http://ssrg.nicta.com.au/projects/TS/20years.pdf

Abstract:
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. In this paper we examine the lessons
learnt in those 20 years in relation to microkernel design. We revisit the L4
design papers, re-examine the approaches and conclusions, and provide
insights into the long-term validity, or lack thereof, of the original
design and
implementation principles. We further examine the design of the seL4 kernel,
which has pushed the L4 model furthest and was the first OS kernel to undergo
a complete formal verification of its implementation. We use the seL4 design to
illustrate how the microkernel has evolved, and to demonstrate the current state
of evolution continues to possess the traits L4 is known for — performance and
minimality.