4 ms·

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

140 points by pjscott 13y ago

kbenson 13y ago
Oh, the conundrum that is the very technical HN story. Do I dive in and devote the time to learn whether this is paper is as interesting as it seems on the surface, or do I wait for some explanatory posts or even a TL;DR summary to help me decide? Edit: The paper helpfully provides much of this itself, with boxed section footers with the change from then to now in how that component is handled. It makes for an interesting way to skim and zero in on sections you may find of interest. e.g. 4.2 Lazy scheduling ends with *Replaced: Lazy scheduling by Benno scheduling"
- panzi 13y ago
  The way to read papers: Read the abstract, if still interested read the conclusion, if still interested read the rest.
  - kbenson 13y ago
    That's probably good in general, I'm not sure how well it holds up to a survey such as this. The paper helpfully assists in this respect though, as I outlined in my edit above.
  - twic 13y ago
    While working as a cell biologist, i followed a different approach: ignore the abstract, look at the figures, if still interested skim the materials and methods, and if still interested, read the rest. The rationale for this is that the most interesting thing is what the authors have discovered, but it's only interesting if they've used sensible and relevant methods, and what is very unlikely to be interesting is the authors' attempt to convince you that the result is stronger and more important than it is.
    - panzi 13y ago
      Yeah, "my" approach[1] is probably best suited for computer science papers. [1] It's not really mine, it's what I was told at university.
- tptacek 13y ago
  When the story is about L4, and the reader is interested in operating systems, the answer to this conundrum is "very yes". L4 is an incredibly simple, elegant, and important OS design. I have a hard time reading about it and not wanting to play around with it (thankfully, I've had the opportunity on projects). Two simple uses for L4: first, as a bare-bones but coherent, complete OS for a purpose-built device; second, as the basis for another OS built on top of it as a "personality". L4 implements most of the hairy parts of an OS (perhaps modulo filesystems), allowing you to build the upper-level OS in terms of L4 abstractions. This paper is a survey of the last 20 years of that microkernel design, which has been picked up and evolved by several teams. One way to approach it would be to read an introduction to one of the original L4 OS's, and then read this one to see which concepts survived into 2014.
greenyoda 13y ago
This article is a PDF document. Here's the 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 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.
Rusky 13y ago
Microkernels are a nice step toward security, but they're a concept ahead of current hardware design and they don't really bring the flexibility typically promised. Services (virtual memory/swapping, file systems, the network stack, etc.) in microkernel systems typically can't be modified or replaced by applications any more than in monolithic kernels, which is probably party of why microkernels have stayed in the realm of embedded systems, etc. where you have control over the whole system. Exokernels bring the flexibility that microkernels don't, by moving the security boundary down the stack. Instead of moving services into trusted user-level processes, they manage protection at the level of hardware resources rather than services. This enables those services to be in untrusted shared libraries that can be securely modified or bypassed on a per-application basis. Thus, instead of the lingering "eh, it's a little slower but we can ignore that," exokernels provide much better opportunities for optimization and tend to be much faster. For example, a database could choose to discard and regenerate index pages rather than swap them out to disk and back; a file copy program could issue large, asynchronous reads and writes of all the copied files at once; a web server could use its knowledge of HTTP to merge packets, or co-locate files from web pages to improve disk seek time. Further, exokernels and microkernels are not mutually exclusive; they are rather orthogonal concepts (you could move an exokernel's drivers into user space processes if you wanted). If we had hardware that were more conducive to a microkernel design, for example with direct process switching rather than going through the kernel (32-bit x86 did this with task gates, but they weren't used much and were abandoned with 64-bit), this would probably be the optimal design, rather than a purist microkernel approach. Incidentally, the in-development Mill CPU design does this very efficiently, as well as a few other things that are good for both micro and exo-kernels.
- nhaehnle 13y ago
  Exokernels tend to be a good idea for quite a number of things. In fact, all modern desktop systems use what is essentially an exokernel design in their graphics driver stack: Rather than implementing OpenGL (or Direct3D or whatever) in the kernel, the kernel drivers provide an interface that allows user space to submit hardware-dependent command lists for the GPU. OpenGL is then implemented as a very thin layer that loads a hardware-dependent user space library. It is this hardware-dependent library that contains the vast majority of the OpenGL implementation, including the shader compilers and everything else that is needed to build the hardware-dependent command list that is ultimately submitted to the kernel.
jacobolus 13y ago
The OOTB/Mill people are apparently working on porting L4/Linux to their architecture: http://millcomputing.com/topic/security/#post-802 http://millcomputing.com/topic/security/#post-802 Their machine-supported security features will be very interesting to see realized.
harry8 13y ago
"For a successful technology, reality must take precedence over public relations, for Nature cannot be fooled." --Richard Feynman All of us need to learn this, re-learn it, revisit it, internalise it, live it and breathe it every day. I'm sure I could do better at attaining such an ideal. So too can these gentlemen.

140 points by pjscott 13y ago

Oh, the conundrum that is the very technical HN story. Do I dive in and devote the time to learn whether this is paper is as interesting as it seems on the surface, or do I wait for some explanatory posts or even a TL;DR summary to help me decide? Edit: The paper helpfully provides much of this itself, with boxed section footers with the change from then to now in how that component is handled. It makes for an interesting way to skim and zero in on sections you may find of interest. e.g. 4.2 Lazy scheduling ends with *Replaced: Lazy scheduling by Benno scheduling"

panzi 13y ago
The way to read papers: Read the abstract, if still interested read the conclusion, if still interested read the rest.
- kbenson 13y ago
  That's probably good in general, I'm not sure how well it holds up to a survey such as this. The paper helpfully assists in this respect though, as I outlined in my edit above.
- twic 13y ago
  While working as a cell biologist, i followed a different approach: ignore the abstract, look at the figures, if still interested skim the materials and methods, and if still interested, read the rest. The rationale for this is that the most interesting thing is what the authors have discovered, but it's only interesting if they've used sensible and relevant methods, and what is very unlikely to be interesting is the authors' attempt to convince you that the result is stronger and more important than it is.
  - panzi 13y ago
    Yeah, "my" approach[1] is probably best suited for computer science papers. [1] It's not really mine, it's what I was told at university.
tptacek 13y ago
When the story is about L4, and the reader is interested in operating systems, the answer to this conundrum is "very yes". L4 is an incredibly simple, elegant, and important OS design. I have a hard time reading about it and not wanting to play around with it (thankfully, I've had the opportunity on projects). Two simple uses for L4: first, as a bare-bones but coherent, complete OS for a purpose-built device; second, as the basis for another OS built on top of it as a "personality". L4 implements most of the hairy parts of an OS (perhaps modulo filesystems), allowing you to build the upper-level OS in terms of L4 abstractions. This paper is a survey of the last 20 years of that microkernel design, which has been picked up and evolved by several teams. One way to approach it would be to read an introduction to one of the original L4 OS's, and then read this one to see which concepts survived into 2014.

greenyoda 13y ago

This article is a PDF document. Here's the 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 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.

Rusky 13y ago

Microkernels are a nice step toward security, but they're a concept ahead of current hardware design and they don't really bring the flexibility typically promised. Services (virtual memory/swapping, file systems, the network stack, etc.) in microkernel systems typically can't be modified or replaced by applications any more than in monolithic kernels, which is probably party of why microkernels have stayed in the realm of embedded systems, etc. where you have control over the whole system. Exokernels bring the flexibility that microkernels don't, by moving the security boundary down the stack. Instead of moving services into trusted user-level processes, they manage protection at the level of hardware resources rather than services. This enables those services to be in untrusted shared libraries that can be securely modified or bypassed on a per-application basis. Thus, instead of the lingering "eh, it's a little slower but we can ignore that," exokernels provide much better opportunities for optimization and tend to be much faster. For example, a database could choose to discard and regenerate index pages rather than swap them out to disk and back; a file copy program could issue large, asynchronous reads and writes of all the copied files at once; a web server could use its knowledge of HTTP to merge packets, or co-locate files from web pages to improve disk seek time. Further, exokernels and microkernels are not mutually exclusive; they are rather orthogonal concepts (you could move an exokernel's drivers into user space processes if you wanted). If we had hardware that were more conducive to a microkernel design, for example with direct process switching rather than going through the kernel (32-bit x86 did this with task gates, but they weren't used much and were abandoned with 64-bit), this would probably be the optimal design, rather than a purist microkernel approach. Incidentally, the in-development Mill CPU design does this very efficiently, as well as a few other things that are good for both micro and exo-kernels.

nhaehnle 13y ago
Exokernels tend to be a good idea for quite a number of things. In fact, all modern desktop systems use what is essentially an exokernel design in their graphics driver stack: Rather than implementing OpenGL (or Direct3D or whatever) in the kernel, the kernel drivers provide an interface that allows user space to submit hardware-dependent command lists for the GPU. OpenGL is then implemented as a very thin layer that loads a hardware-dependent user space library. It is this hardware-dependent library that contains the vast majority of the OpenGL implementation, including the shader compilers and everything else that is needed to build the hardware-dependent command list that is ultimately submitted to the kernel.

jacobolus 13y ago

The OOTB/Mill people are apparently working on porting L4/Linux to their architecture: http://millcomputing.com/topic/security/#post-802 http://millcomputing.com/topic/security/#post-802 Their machine-supported security features will be very interesting to see realized.

harry8 13y ago

"For a successful technology, reality must take precedence over public relations, for Nature cannot be fooled." --Richard Feynman All of us need to learn this, re-learn it, revisit it, internalise it, live it and breathe it every day. I'm sure I could do better at attaining such an ideal. So too can these gentlemen.