| ▲ | upboundspiral 2 hours ago | |
I would like to qualify that seL4 (and the entire family of L4 kernels) were created exactly to disprove the idea that microkernels were slow. They are extremely perfomant. The idea that microkernels are slow came from analyzing a popular microkernel at the time - mach. It in no way is a true blanket statement for all microkernels. edit: found a good comparison chart (first link) https://sigops.org/s/conferences/sosp/2013/talks/elphinstone... https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/performance.html | ||
| ▲ | gucci-on-fleek 2 hours ago | parent [-] | |
> The idea that microkernels are slow came from analyzing a popular microkernel at the time - mach. It in no way is a true blanket statement for all microkernels. Don't microkernels inherently require lots of context switches between kernel-space and user-space, which are especially slow in a post-Meltdown/Spectre world? I know that Linux has semi-recently added kTLS and KSMBD to speed up TLS/SMB, and Windows used to implement parts of font rendering and its HTTP server in kernel mode to speed things up too, so this gave me the impression that having more things inside the kernel (== more monolithic) is better for speed. Or is this only the case because of how the Linux/NT kernels are implemented, and doesn't apply to microkernels? | ||