> Where I believe general purpose microkernels have struggled is in the performance of the messaging (often because of the increased access checking).

Jochen Liedtke's work on the L4 kernel family showed that microkernels can be really fast.