Skip to content

Where Andy is wrong about L4

2012/02/15

Andy Tanenbaum, in a recent interview with LinuxFr.org, made some comments about L4. Unfortunately, they were mostly wrong.

Make no mistake, Andy is a guy I hold in high regard, he’s done great things over the years. But that doesn’t mean he should get away with making incorrect statements about the main competitor to his Minix system! And I’m not fussed about the outdated number of 300 million L4 deployments (the official figure is 1.5 billion). There are far more substantial issues. So, let’s have a look at what he said.

Andy Quote 1: “The biggest difference is that we [Minix] run the entire operating system as a collection of servers in userland. They [L4] mostly run Linux as a whole unit in userland. This means that a single bug in Linux can crash Linux. While L4 will survive this, all that does is make the reboot faster. It doesn’t solve the reliability problem.”

While it is true that L4 is being used as a virtualization platform to host Linux (something my colleague Hermann Härtig in Dresden has been doing since 1997), and there are phones out there that run Linux on top of L4, that isn’t the whole story. In fact, if all we did was put L4 underneath Linux, we’d do nothing than adding overhead. Clearly, that would be a pointless exercise.

There are several reasons why you’d want to run Linux on top of L4. One is the classical virtualization use case of processor consolidation: running multiple systems side-by-side on the same processor, using virtual-machine encapsulation to isolate one from the other. This is the configuration that is indeed used on some of the phones that ship with L4.

The second reason is legacy support: If you think you can just introduce a new OS API (even if it’s POSIX-compliant) and the world will adapt all its software, you’re dreaming. People want to not only keep re-using their old software, they even want to build new software to the old environments. But that shouldn’t stop you from providing a better environment for safety- and security-critical components.

This trend is indeed very strong in the embedded world, even (or particularly) in the domain of safety- or security-critical devices. I rarely get to talk to someone considering deploying seL4 who doesn’t have a need for a Linux or Windows environment. The important point is that a highly trustworthy microkernel underneath allows this to co-exist safely with the critical functionality.

Andy Quote 2: “There are lots of technical differences between MINIX and L4, but the focus of the projects is very different. We [Andy] have a microkernel so we can run a multiserver system. The entire focus is on multiserver and the ability to restart OS components independently. L4 is being used to run Linux and on phones. This has nothing to do with technical differences. We could have used L4 and they could have used MINIX but it is easier to use your own since you can change it as needs arise.”

Notwithstanding my comments above, the reality is that many of the 1.5 billion L4 deployments have nothing whatsoever to do with Linux! They run L4 on the baseband processor of a smartphone, with Linux (or Windows or iOS or BBOS or xyz) running on a separate applications processor. And the baseband stack is in fact a multi-server design! It consists of multiple (each multithreaded) tasks that communicate with each other. Exactly what Andy claims he does and we don’t…

The statement that “they” (i.e. us) could have used Minix is actually quite wrong. Minix, owing to its design and strong emphasis on simplicity, is much slower than L4. (Their papers typically tell you that throughput is only degraded by a few %. However, that’s typically compared to Minux-2, which isn’t the world’s fastest system either, while a reasonable baseline would be Linux. Furthermore, they don’t tell you how much CPU usage increased – I’ve discussed this with Andy, and unless things have changed a lot recently, then CPU overhead is pretty significant. Pretending that throughput degradation measures overhead while ignoring CPU load is one of my favourite benchmarking crimes!)

Performance happens to be pretty important on a mobile device (whether it’s a phone or an implanted medical device). Throwing away cycles means throwing away battery life, and manufacturers tend to care about this. In my experience, overheads of more than 5% (measured in terms of CPU cycles) are considered unacceptable in this space. Minix certainly wouldn’t be useful in a mobile environment at all!

Andy Quote 3: “They certainly did a nice job [on formal verification of seL4] but it is really hard to verify if it works since the hardware itself is poorly defined and the OS has to deal with the hardware a lot.”

C’mon, Andy, that one’s really cheap! seL4 is the first (and so far only) OS kernel which has a formal (mathematical and machine-checked) proof that its implementation follows the specification. That means nothing less than that the implementation is bug-free with respect to the spec. Something that just cannot be achieved by simplicity and any amount of code inspection or testing!

Andy seems to imply that because the hardware isn’t exactly defined, the verification is somewhat worthless. Of course, if the hardware’s behaviour isn’t defined well enough, then that hurts Minix just as well. But the argument is actually bogus. The verification of seL4 was done for ARM processors, and (unlike x86) they have a very precisely-defined ISA. It’s so well defined that Anthony Fox and Magnus Myreen at Cambridge could turn it into a formal (mathematical) model. And we’re in the process of linking this model to our seL4 code proof.

In reality, the functional correctness proof of seL4 is very powerful. It means that seL4’s behaviour is very precisely defined (there is a formal spec of the kernel). And the implementation adheres to that spec. Which means that in order to prove safety or security properties of a system built on top, it is generally sufficient to prove that these properties hold with respect to the seL4 spec, and by implication they hold for the system. (I’m glossing over a few details here, this argument requires more than functional correctness. However, all the other bits required are either already in place for seL4, or we’re working on them and they should be in place this year!)

So, how about the multi-server issue? This is the classical microkernel approach: you structure the microkernel-based system into multiple components (or servers) and the microkernel enforces isolation between them. This can lead to a more fault-tolerant system, as Andy keeps pointing out (correctly). However, if he seems to imply that this somehow is different from what we do, then that’s simply wrong. In fact, our Trustworthy Systems research agenda uses exactly this component approach. The difference is that we can prove (security or safety or other) properties of our system. No-one else can do this!

On top of that we have a few other cool bits. Such as device drivers which are synthesised from formal specs, and are as such correct by construction! Perfect complement to a formally-verified kernel.

Andy Quote 4 (not actually about L4 but about capability-based OSes like Coyotos): “Capability systems have been around for 40 years. At the recent SOSP conference, M.I.T. professor Jack Dennis got an award for inventing them in 1967. They definitely have potential. My first distributed system, Amoeba, used them. Coyotos, however, is going nowhere.”

Am I to read this as an argument that because CoyotOS is going nowhere, capability systems aren’t?

seL4 is a capability-based system too. And, unlike CoyotOS, it is going places! In fact, capabilities are a core part of the safety/security story in seL4: they allow us to reason precisely about access rights (and information flow) in the system, in a way that is impossible to do with an access-control-list based approach as Minix uses it.

Summary

The two approaches are similar as far as OS structure is concerned. The core difference is that with Minix, Andy is trying to get things right by keeping them really simple. He cops a significant performance overhead, yet in the end can only use traditional quality-assurance methods (testing and code inspection) to make a case about the behaviour of his system. Nor can he formally reason about the security/safety properties of the complete system.

In contrast, with seL4 we have a microkernel that is blindingly fast (as fast as any L4 kernel, and no other microkernel has ever been able to beat L4 in performance), yet we can make actual guarantees about its behaviour and that of systems built on top, with the strength of mathematical proof!

Everything else is simply not playing in the same league.

Advertisements
8 Comments
  1. What is the best L4 kernel to implement a multi-server OS?

    I’m relative new to L4

    Thank you,
    Cheers

  2. seL4 has the right mechanisms which were missing in earlier L4 versions. Fiasco probably has them too.

  3. Yuji ota permalink

    I have some question about advantage of micro kernel architecture because I’m trying to write small desktop operating system as my hobby 🙂 I’m very glad if you could answer my question or write some topic about my questions. (Sorry for my bad English and long post…You may feel rude or saucy about my English, but I’m not intend it)

    …and Here is my questions.

    1. Is micro-kernel architecture suitable for “desktop” operating system?

    I know Desktop/Laptop computer is obsolete nowadays because everybody went mobile devices. but I’m interested in writing Linux clone based on micro-kernel architecture. I choose this topic because I studing about OS development from Tanenbaum’s text book and want to know the winner of “Torvalds-Tanenbaum framewar” XD. (And I have lot of time so far…)
    Seriously I found QNX is widely used for “embed” system but there is no popular micro-kernel OS for “desktop”. I want to know why. GNU hurd is the one, maybe, but it’s still “under construction”. Is it so difficult to build micro-kernel runs on desktop machine?

    2. Micro-Kernel architecture is essential for enough modularity?

    I read an article that Linus Tovals admit Linux is too complex nowadays. But I think this is not a problem of operating system architecture. Just merged too much code on main line. using loadable kernel module, kernel size could be reduced I guess…Is this wrong? If implementation and maintenance policy is good, Monolithic kernel can be enough modular and compact I guess. (Of course if Linux was micro-kernel architecture, additional file-system and driver has not to be merged in a first place…and more easier to add experimental feature or debug. but focus on only “modularity”, Monolithic kernel can be enough modular I think…)

    …Sorry for *really* long post but I have two more questions (I couldn’t find email address so post on related topic).

    3. I want to know about advantage of micro-kernel on relatively small multi-processor environment. I’m thinking about desktop computer which has 2 ~ 16 core in the processor. not a big cluster.

    I read some article about Linux developer struggling with replacing “kernel lock (aka, giant lock)” with spin lock or semaphore. It seems used for resource exclusion between threads…and it looks soooo complicated. In micro-kernel architecture, resource exclusion in muliti-threading can be implemented more “smart & clean way”? If it is, how?
    (Actually, I found the slide you wrote about this topic
    http://www.ssrg.nicta.com.au/publications/papers/Heiser_08lca.slides.pdf
    but want to know more…If you know some technical paper or book about micro-kernel implementation on multi-processor please let me know!)

    this is a last question…and I want to say “thank you for reading :)”

    4. Is it possible to write powerful micro-kernel operating system which run on desktop/server computer? (Or it exists already?)

    Now Linux has strong code base and de-facto standard of unix like operating system in open source community. And I think it’s good. Because at least for my personal purpose, all those Monolithic operating system (Windows, Linux) work fine…but those operating system is almost 20 years old. now usual desktop computer have 2 ~ 4 cores and big cpu cache. ipc cost is reduced by the processor feature like tagging-tlb. If write new micro-kernel operating system today, It’ll be very cool.

    Thank you for reading my poor and really long post. but I really wanted to know about latest operating system architecture which I can study/develop.

    • Apologies for letting this sit in the queue for a while.

      Re your questions:

      1. “Is micro-kernel architecture suitable for ‘desktop’ operating system?”

      Sure, there is no reason why a desktop OS couldn’t be microkernel based. Minix-3 is actually doing this. (Their poor performance probably limits use severely.) GreenHills also has a desktop OS environment based on their Integrity microkernel. I understand performance issues are similar. The Hurd is pretty dead from what I can tell. There actually used to be a desktop version of QNX, but that has been abandoned a long time ago.

      You could certainly do better with L4, but it’d be a big project. For a desktop you need a lot of functionality, and if you’d want it to work well, you’d have to implement a lot of it from scratch, or massively re-engineer existing components out of Linux etc. And it would require a lot of systems-building experience to develop a highly componentised systems that isn’t hopelessly slow.

      2. “Micro-Kernel architecture is essential for enough modularity?”

      If you want to enforce modularity in the OS then you either need to use a microkernel (hardware-enforced isolation) or use a typesafe language (as in Singularity, but note that their trusted runtime is actually significantly bigger than L4, and their performance is worse).

      3. “I want to know about advantage of micro-kernel on relatively small multi-processor environment.”

      We think we can get away without fine-grained locking in the kernel, without impacting performance. This is a consequence of system calls in a well-designed microkernel being short, and a big lock therefore not highly contented on a small to moderate number of processors. We’re actually presently working on a paper to show that this is actually true, so I can’t give you a definite answer yet.

      4. “Is it possible to write powerful micro-kernel operating system which run on desktop/server computer?”

      I think I answered this already under (1): Yes, it should be possible, but it’ll be a lot of work, and I’m not convinced it makes economical sense.

      Gernot

  4. Andy is criticizing the implementations, and he’s not technically incorrect, but he’s wrong about L4 in totality. You’re also wrong for defending the deeply flawed implementations, and show a troubling lack of vision. On the points,

    ” if all we did was put L4 underneath Linux, we’d do nothing than adding overhead. Clearly, that would be a pointless exercise.”

    Damn straight, but that’s all we’ve done for more than a decade. While this has some very useful edge cases, it’s not beneficial outside the embedded space. This is clearly demonstrated by how difficult it’s been to move L4 to general purpose systems. It can be done and the payoff would be immense, but it would require hard work and a clear vision…. both in short supply around L4.

    “if you think you can just introduce a new OS API (even if it’s POSIX-compliant) and the world will adapt all its software, you’re dreaming”

    True if created a new API, you will fail towards general purpose. The reason is simple, people need their software, and software is extremely time consuming to create. Most importantly is not about users, who theoretically could run their software through inefficient containers, but system software which would require a complete rewrite.

    You then conclude because a new API is a terrible option, you cannot use the current API’s. This is where you’re beyond incorrect, and once again lack total vision. This is my complete vision, and if I had half the talent of you and your team I’d be a keynote speaker.

    1. Modern L4 Kernel

    – Task completed

    2. Complete implementation of the following POSIX 2008 Specs,

    – Base Definitions, Issue 7
    – System Interfaces and Headers, Issue 7

    3. epoll Implementation

    – providing epoll.h

    4. implementation of DRM KMS Framework

    – providing fb.h and drm.h

    5. Mesa Library

    6. DDE-Kit, or IOkit

    All these interfaces must be implemented as close to that kernel as possible, isolation will destroy the entire premise of avoiding mass system software rewrite. The L4 provided, userland API should only be used to implement the system level interfaces. The end-user should only require the POSIX/Linux implemented APIs.

    On these interfaces you can now EASILY port Wayland, and KMSCON. Widget toolkits already support Wayland, and Weston on Wayland is your compatibility X server.

    Porting the last POSIX 2008 Spec, on the previously implemented POSIX APIs.
    – Commands and Utilities, Issue 7.

    You would finally need a way to manage users, and you must avoid system software rewrite, so lastly port DBUS and Systemd.

    DONE, the system is now drop-in replaceable for Linux, after libraries are recompiled on this base.

    So it’s beyond possible, it’s beyond theoretical, and should have been started 5 years ago.

    • Apologies for my lack of vision, I just happen to think that there are more interesting/important/cool things to do than re-implementing outdated system APIs. I’m actually more interested in rather more fundamental changes (see this recent talk for an idea of what I’m thinking of, although it may be a bit difficult to get the story from just looking at slides).

      What you’re asking for is IMHO a pure engineering effort. This sort of stuff is fine for volunteers, or industry (if someone can come up with a business case). My funding sources would be unimpressed if I was blowing their tax dollars on engineering projects. Nor would my students be motivated to do such a thing.

      Besides, there’s little chance of getting traction with a new OS in the desktop/server space, there is just no compelling benefit. Linux made it because industry wanted to break the Microsoft monopoly, and was willing to invest billions in doing that (and it literally took billions!) Not likely to happen again.

      Gernot

      PS: Sometimes you can actually do cool stuff by running Linux in a virtual machine, see RapiLog.

  5. Pez permalink

    As long as the currently mainteined L4 implementations are closed source (except for NOVA) L4 is CLEARLY going nowhere… Minix, BSD, Mach and Linux are open, they go ahead. Or is the case some *important* machine is running L4 outside Germany? Let me know when a free, usable, downloadable version of an L4 based operating system is available. Then, only then, you can say Mr. Tannenbaum is wrong, and your baby is good.

    • Well, the truth (or lack thereof) of Andy’s comments are independent of open or closed source.

      However, you seem to have missed a few things during the last 20 years.

      Firstly, mose L4 versions are open-source:
      – The Dresden Fiasco (L4Re) kernel has been open-source since it was written in 1998
      – The Karlsruhe Pistachio kernel has been open-source since it was written in 2002, our L4-embedded fork since we did it in 2004
      – Our seL4 kernel has been open-source since July 2014.

      Secondly, a *lot* of stuff is running on L4:
      – Qualcomm modem chips have been running our L4-embedded kernel since 2006, that’s a few billion devices
      – The security processor of all iOS devices is running a modified version of our L4-embedded, that’s another 200-300 million devices every year
      – seL4 is being deployed on autonomous military air and ground vehicles, with the first autonomous helicopter flight in July 2015
      – many other safety- and security-critical deployments are in progress.

      I’m not aware of any real-world deployments of Minix.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: