Comment by darksaints
2 days ago
True, but the last time I checked (several years ago), the size of the portion of code that is not drivers or kernel modules was still 7 million lines of code, and the average system still has to load a few million more via kernel modules and drivers. That is still a phenomenally large attack surface.
The SeL4 kernel is 10k lines of code. OKL4 is 13k. QNX is ~30k.
Can I run Firefox or PostgreSQL with reasonable performance on SeL4, OKL4, or QNX?
SeL4 was not built for multiple CPU cores, it's not going to perform with modern day "high end" hardware and last I looked its formal proofs don't apply to multicore systems.
Reasonable performance includes GPU acceleration for both rendering and decoding media, right?
Not necessarily; short-comings or "TODO"s are okay. I just want to know if I can run actual real-world complex applications on these micro-kernels, and what the trade-offs are (if any). Firefox on OpenBSD has fairly reasonable performance, but is quite a lot slower than on Linux. It's a perfectly reasonable trade-off, but you do need to be aware of it.
I've asked this question a few times over the last few years when people bring up "we must use microkernel now! They already exist!"-type posts, and thus far the response has either been crickets or vague hand-waving with microbenchmarks that bear no relation to real-world programs.
yes