Worth noting are modern (gen2/3, L4 onwards) microkernel context switch costs.
This article has a neat table in it. Third page.
http://sigops.org/sosp/sosp13/papers/p133-elphinstone.pdf
In contrast, Linux takes whole microseconds. This should be carefully considered when thinking about multiserver architecture overhead.
I'd love to hear otherwise or in more detail from someone at Google. It's frustrating to have to do archaeology just to guess what the state of the art is. Isn't sharing your findings part of "organizing the world's information"?
It's the bit on the end that sounds a lot less noble.
In the case of seL4, they are WCET (Worst Case Execution Time). That's as "contended" as it can possibly get.
They do provide formal proof of WCET, so these numbers are solid.
[edit]
Also formal WCET analysis for various IPCs is really great and not something you can "bolt on" to a kernel not designed for it.
Specifically:
Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser
Timing analysis of a protected operating system kernel
IEEE Real-Time Systems Symposium, pp. 339-348, Vienna, Austria, November, 2011
---
TL;DR: They assume worst case for cache misses.
e.g.: "The latency of a read or write to physical memory on this platform was measured to be 80–100 cycles; in the static analysis we assume a 100-cycle penalty for all cache misses."