>IPCs are slow and the gains are limited compared to the strategies all broadly used kernels already use.
The problem you are describing is a characteristic of 1st generation microkernels, and was solved by Jochen Liedtke in the mid 90s, introducing 2nd generation microkernels.
seL4 is a 3rd generation microkernel.
>I don’t know what "modern" microkernel means.
To get up to date, a good resource is Gernot Heiser's blog[0], read from oldest to newest.
It’s not about being up to date. What you call modern here is just recent. It doesn’t fundamentally diverge from the historical architecture.
Even SeL4 fast IPC which is not actually a full IPC but works well in the barebone context of SeL4 remains in fact slower than good old syscalls.
The fundamental question remains the same “Is this worse the costs (in terms of both efficiency and design complexity)?”
To me, the answer is muddy here. Sometimes yes, sometimes probably not. I think it’s why hybrid approaches are now generalised but no one is really shipping a microkernel outside of industrial applications.
The problem you are describing is a characteristic of 1st generation microkernels, and was solved by Jochen Liedtke in the mid 90s, introducing 2nd generation microkernels.
seL4 is a 3rd generation microkernel.
>I don’t know what "modern" microkernel means.
To get up to date, a good resource is Gernot Heiser's blog[0], read from oldest to newest.
0. https://microkerneldude.org/