I'd thought I mention a kernel that I am intensely curious about, but which also seems pretty unknown in the community, that kernel is L4.
L4 is a microkernel, designed by Jochen Liedtke, it is a high-speed microkernel written primarily in assembler.
The orignal design, was to develop a microkernel, that tries to impose as little policy as possible on the full operating environment (sound familiar!).
The end result, L4, was a fast real-time, multi-threaded microkernel. It's primary benefit being extremely fast IPC (inter process communications), which reduces the overhead of pushing traditional kernel processes into user space.
The approach taken with L4 opposes that taken with Hurd, in that the kernel is heavily optimised for a particular architecture (indeed even specific instances of an architecture). This optmisation is deemed necessary to ensure maximum kernel performance, and negate arguments against microkernels being too slow, as demonstrated with Mach and the Hurd.
To prove the viability of the L4 design, they built L4Linux on top of L4, as a monolithic server. The amazing thing is that the performance reduction was only 10% on average. Paper here.
While I say monolithic server, functions of the Linux kernel were still split of into different threads. However only the bare minimum to get it working. The implications of this are that the use of L4, as a base, and increasingly splitting up Linux into different servers could very well improve Linux performance, as well as making it a good environment for real-time computing, and low-latency work (Audio and video). This is indeed the aim of IBM's Sawmill project .
The problem with L4 is, that at the moment the Code is non-free, and the only version available is an old one from 1995. I believe that there are talks underway to GPL it. However, there are projects such as L4/Fiasco to produce a C++ version of the Microkernel, albeit however with the performance drawbacks of using such a language.
So L4, to me, seems to have everything required of a microkernel. Are more architecture dependent kernels the way to go? I can't say for sure, but I think the general basis is sound, and porting an optimised microkernel probably takes about as much effort as porting the hardware dependent components of Linux to a different architecture anyway, so portability is not a factor (although feel free to prove me wrong!).