Some weekend reading.  I really enjoyed this one about lessons from 20 years of the L4 microkernel.  (Before I read this I couldn't have told you anything about L4 vs Mach vs any other microkernel, but it was readable despite that.  If I was writing super-low-level device firmware, this design sounds like something I'd appreciate.  The way user processes "donate" memory to make room for kernel objects seems really clever.)

http://www.nicta.com.au/pub?doc=6930