Are those really WCET? A L3 miss on an i7 4770 is ~60ns and they show 90ns total execution time. If that's true it's incredibly impressive.

[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.

You might want to look into: http://ts.data61.csiro.au/projects/seL4/

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."

That would mean ~2 cache lines are accessed for an IPC call, plus another 130 cycles for instructions. That's very impressive.