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.
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
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.