[erichocean]

The major source of errors in a kernel is device drivers, and Linux typically is running many more drivers than the embedded kernels you mentioned. Look at any Linux point release: the majority of churn is in driver code, to fix bugs.

Thus, it stands to reason, Linux is likely less stable than an embedded kernel without all that driver code.

I run a pre-emptive embedded kernel (QK) that's extremely tiny and, in fact, was validated by myself with KLEE (a symbolic checker) to exhaustively verify correctness. I'm certain it's more reliable than Linux, which carries no such guarantee (and is orders of magnitude larger -- even excluding driver code).

Bug rates correlate extremely close with lines of code. All else being equal, a large system has more bugs, simply because it has more opportunity for them.

If you truly care about correctness, doing formal verification, model checking, etc. is the way to go, not "lots of people use it so it must be stable".

To benefit from formal verification, you have to design your code around that, and most systems today are not. It's hard to retrofit verification on top of a legacy codebase like Linux.

[javert]

I don't really understand your driver argument, because when deploying Linux on an embedded system, you would only use the drivers you need... so you'd have the same amount of driver code as with any other kernel.

You say that you managed to "verify correctness" on QK, but clearly, that's not an accurate statement, since AFAIK seL4 is the only kernel that has ever been "proven correct" (and even for seL4, there are some gotchas there, AFAIK).

If you truly care about correctness, doing formal verification, model checking, etc. ...

The common perception is that model checking and formal verification are still just research areas that can't be used practically beyond toy problems. Again, seL4 is the only kernel I know of that has been "proven correct," and that has taken an insane amount of manpower that is not scalable to anything more complex than seL4. That seems to be evidence that there is something to the "common perception" I stated above.

lots of people use it so it must be stable

That's not really my argument. With Linux, there is an insane amount of testing going on all the time (I mean "informal" testing.. just people using it and reporting problems if they encounter any.. though there are also farms set up that test Linux, as well). Linux must be by far the most highly-tested software in history. On the other hand, you could use formal methods on some small kernel and maybe get some help (but again, far short of proving there are no bugs, AFAIK), but the level of testing will be many orders of magnitude less. Clearly, which one wins out depends on how good the actual state of the art in formal methods is, but my impression is that many orders of magnitude more testing will win out, unless the problem you are solving is very, very small.

[erichocean]

The entire QK[1] kernel, including all library code, is less that two thousand lines of C (and most of the library code isn't even used by the kernel itself, which is just 234 LOC). QK is a single-processor kernel (although still pre-emptive) and very well written and tested (in, literally, hundreds of millions of devices).

It was not difficult at all to run QK and it's supporting code through KLEE and exhaustively verify the properties of each function, thanks to a super-simple design and the many included assertions, preconditions, and postconditions, which KLEE helpfully proves are satisfied automatically. If I wanted a certified optimizing C compiler, I'd use CompCert[2] to compile QK, which would give me a certified kernel all the way to machine code. (I actually use Clang.)

I am familiar with the verified L4 kernel, and it is far more complex than the QK kernel I have verified. That people have already verified a kernel far more complex should be sufficient proof that a much simpler kernel can also have its correctness verified.

Stepping back, it's 2012: people should no longer be surprised when a small-but-meaningful codebase is certified correct. It's common enough now that you don't get published in a journal just because you did it.

[1] http://www.state-machine.com/qp/index.php

[2] http://compcert.inria.fr/

[javert]

By the way, I am going to look into actually applying KLEE to some of my own code. I had heard of it before, but thanks for bringing it up, I hadn't really given it much thought until now.

In my research, I'm trying to write a "fancy" task scheduler at the user level, so that someone can get "fancy" scheduling policies without modifying the RTOS kernel. By "fancy" I mean fully preemptive and allowing "interesting" scheduling policies/synchronization protocols to be implemented. "Interesting" generally means multicore, in my particular research community.

If you don't mind me asking, what kind of projects do you/have you used QK for?

[javert]

Interesting. I had never heard of QK, and I'm slightly surprised about that.

people should no longer be surprised when a small-but-meaningful codebase is certified correct

For the size of codebase you're talking about, I'm not really that surprised. But I still think that formal methods don't scale to multicore RTOSs, which is the area I study (I'm a CS grad student).

[davidw]

So I think it'd be fair to say that Linux does ok in the robustness / lines of code or robustness / devices and real world interfaces, however, in terms of absolute numbers, a smaller system is almost always going to do better.