4 ms·

Except that it is again a comparison with Mach, what's the size of L4?

• vezzy-fnord 11y ago
  It's a red herring, anyway. Microkernels aren't so much about size as they are about separation of concerns. Otherwise we'd have to conclude V7 Unix and DOS are both microkernels, which is preposterous.
• hga 11y ago
  The verified down to the machine code and GPLed seL4 is only 9,000 line, and some of those are largely artifacts of the hand translation from Haskell to C. On the other hand, it doesn't do all that much for you, there's a lot of kernel type behavior you have to implement above it. But you are starting out with a relatively very small Trusted Computing Base (TCB).