3 ms·
You're not just living in a dream world, you're using the phrase to excuse a snide strawman. The Linux kernel is 12-20 million lines of code depending on how y
by nieve 12y ago
You're not just living in a dream world, you're using the phrase to excuse a snide strawman. The Linux kernel is 12-20 million lines of code depending on how you count it (and how far up the top end has gone recently). It is not possible for humans to know and comprehend the entire codebase, much less avoid all lockup bugs by reasoning about the code. In fact I'm pretty sure all extant methods of creating a correctness proof fail at that scale (even if you can ignore drivers). Much of the kernel requires specialized skills and experience the majority of kernel developers don't have.
Beyond that the kernel developers value both correctness and performance. Most of these bugs involve multiprocessing and a huge amount of effort has gone into getting rid of them global locks, but even they aren't easy to reason about at that scale - I think you're missing the common thread in "deadlock" and "Global Interpreter Lock". Pretending that a world could exist where we can simply reason about something like the Linux kernel and then using it to state that devs can simplify or improve the logic is taking a completely unsupported cheap shot and the disclaimer about the real world doesn't change that. I'm not even sure what your motivation for the equivalent of "if you pretend that friction & drag don't exist it's really easy to figure out aerodynamics, so plane designers need to do better" (hint, it's not) is, but it certainly isn't to inform, contribute, or facilitate the debate.
- mrich 12y agoWho says a kernel must have 15 million lines of code? I'm pretty sure there are kernels out there that have been verified correct. Of course the hardware could still be broken (can also be proven correct) or a cosmic ray could flip some bits...
- lomnakkus 12y agoL4 was verified (mostly, at least): http://ertos.nicta.com/research/l4.verified/approach.pml http://ertos.nicta.com/research/l4.verified/approach.pml
- Someone 12y agoDivide and conquer. For every modular part in the kernel, define what it is supposed to do: are calls reentrant? What combinations of calls are allowed? What interrupts can it generate? Etc. If you don't make rules as to how the parts are to behave, how are writers of device drivers going to know how to make a working driver? Tweak it until it doesn't hang the system in a few days? And how are you going to fix that deadlock you find during debugging? You may know (simple exampe) that thread T1 holds lock L1 while trying to get L2, while thread T2 holds L2 while trying to get L1, but without guidance on how things are supposed to work, how do you even know whether to fix T1 or T2? IMO, the more complex the system, the greater the need for simpe rules that limit what different parts can do. Chances are there will still be lockup bugs, but that is not a reason not to try and avoid them.