Yeah its funny what we can get away with using different design tradeoffs on modern computers.

I've been reading through the SeL4 source code lately. SeL4 isn't a multithreaded kernel. It supports SMP - so, it can use all the cores on your computer. But the kernel itself uses a big mutex. Complex syscalls can't run concurrently.

And you know what? I think its fine. A tiny microkernel like SeL4 offloads almost everything to separate processes anyway. The only things in the core kernel are the bootloader, scheduler and thread cap tables. Device drivers are multithreaded because they all run in separate processes.

Having the kernel itself effectively single threaded reduces a whole class of bugs and complexity, at a (hopefully) negligible performance cost. Its smart.