Hacker News Reader

Comment by strictfp | Hacker News Reader

Remember that microkernels aren't just trying to achieve modularity - they also take a stab at robustness by failure recovery. This is IMO doomed to fail - you are much better off trying to achieve robustness by correctness. Monolithic kernels focus more on correctness and therefore progress much faster.

View on HN

Most of the kernels that try very hard to achieve correctness (in the embedded / real-time space that would be used in military or aerospace applications) are microkernels. Microkernels have a smaller number of primitives that are more orthogonal, so they are easier to implement correctly and audit them, and you get some amount of preemptibility for free.

Also, as far as I know, the only kernel that has been proven correct with a mechanically verifiable proof is an L4 variant.

proven correct with a mechanically verifiable proof is an L4 variant

seL4, which is microkernel of course

http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf

MINIX seems to be working pretty well these days.

Monolithic kernels don't "focus on correctness". Some people might when writing one, plan 9 for example. But plenty don't, like linux as the most obvious example.

Interestingly, important parts of the Linux kernel are proven correct (e.g. the scheduler). But yeah...not the whole thing.

What? When and where has any part of linux been proven correct?

Reading the Plan 9 kernel code hasn't convinced me that its authors focused on correctness. The kernel code is pretty, and its twenty-year-old architecture could pass as only ten years old; but even excluding drivers, there is no shortage of bugs.

You found lots of bugs reading the plan 9 kernel source, and forgot to report them?

What I mean is that they try to achieve stability by eliminating bugs, not by doing damage control. Proactive vs reactive.

And what I mean is that is simply not true. Monolithic kernels give us unstable systems like windows, linux, BSDs, etc. Virtually ever highly reliable operating system is built on a microkernel.

Reply on news.ycombinator.com