[Rochus]

That all sounds very interesting, but it goes far beyond the scope of my current concern with microkernels. At the moment, I am satisfied with extending a well-documented approach such as Minix with sel4 (or other candidates) in such a way that the performance meets contemporary expectations. With regard to Parnas' approach, there is still considerable scope for possible solutions, as he has formulated conceptual ideas rather prescriptions and policies. I can understand your fascination with new, previously untried approaches, but considering that Tanenbaum's book is already twenty years old, there is obviously a gap in the literature on the proven state of the art that should be closed.

[vacuity]

This is mostly untreaded territory, true, but I think going to extremes is instructive for moderation. In this kernel or others, abstractions can be created to build back up to what we are used to, but going far afield is necessary to remake the core. I was also thinking about the process of proving out solutions, and my arguments largely appeal to the existing groundwork of seL4 and Barrelfish, though of course they are still fairly unproven. I use many other works for inspiration for smaller parts of the design, such as scheduler activations or Nemesis' self paging, and they're easier to apply to other OSes. It is great to see Linux gradually proving technologies that have long been imagined, such as increasing userspace agency in handling segfaults, and the longstanding question of modular schedulers. The nice thing about principles such as what Parnas described is that they are always worth considering. My ideas must be concretely implemented, but the true benefit will lie in how they inform our understanding of the abstract solution space. I'll be happy if my work leads to more microkernel-like work in Linux!