3 ms·
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
by strictfp 13y ago
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.
- rookieMP 13y agoMINIX seems to be working pretty well these days.
- cwzwarich 13y agoMost 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.
- lelf 13y agoproven 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 http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
- papsosouid 13y agoMonolithic 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.
- m0th87 13y agoInterestingly, important parts of the Linux kernel are proven correct (e.g. the scheduler). But yeah...not the whole thing.
- papsosouid 13y agoWhat? When and where has any part of linux been proven correct?
- p9idf 13y agoReading 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.
- papsosouid 13y agoYou found lots of bugs reading the plan 9 kernel source, and forgot to report them?
- strictfp 13y agoWhat I mean is that they try to achieve stability by eliminating bugs, not by doing damage control. Proactive vs reactive.
- papsosouid 13y agoAnd 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.