It's interesting how it's Obviously Impossible to write OSes in garbage-collected languages, and this is proven by the fact successful OSes were written in garbage-collected languages back in the Stone Age, or 1980s, whichever. My current laptop has enough RAM to swallow the entire state of a Symbolics workstation (RAM and disk) without noticing, but it's obviously too wimpy to run an OS written in anything other than C.

(Nitpickers' Corner: "Successful" and "the most commercially successful" are, in fact, two different words. Gots all them different letters an' everything. Therefore, Genera not being as profitable as such Sophisticated Top-Of-The-Line Pieces of Professional-Grade Enterprise-Ready software as MS-DOS doesn't mean Genera wasn't successful.)

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.

My android with garbage collected userspace challenging Termux folks, works just fine....