The famous Tannenbaum-Torvalds debate happened all the way back in 1992. At the time, the most common microkernel was Mach, which had significant performance problems. NeXT/Apple solved them by transforming Mach into a monolithic kernel, making Mach (as XNU) one of the most popular kernels in the world today (powering iPhones, iPads, Macs, etc). But that doesn’t help Tannenbaum‘s side of the argument. And I don’t believe his own Minix did much better than Mach did.
Whereas, from what I hear, L4 and its derivatives have solved this problem in a way that Mach/Minix/etc could not. Yet still, it makes me wonder, if L4 has really solved it, why aren’t we all running L4? L4 has had some success in embedded applications (such as mobile basebands, Apple Secure Enclave); but as a general purpose operating system has never really taken off.
An application in which something like slow file IO wouldn’t be a problem - does it even have a filesystem? And we don’t know whether Intel has done things to make it an “impure” microkernel, like what NeXT/Apple did to XNU, or Microsoft did with win32k.sys
