Given the recent discussions re IPC performance, I thought it’d be helpful to summarise the state of the art. I’ve put up a performance page on http://l4hq.org (linked from the home page) showing IPC latencies of various L4 kernels across 20 years of architectures. It’s an expanded version of what’s in [Elphinstone & Heiser, SOSP’13]. Each entry in there is, AFAIK, the fastest ever-reported IPC performance of any full-semantics microkernel (i.e. not jsut L4, it’s just that no non-L4 kernel ever broke any records in the last 20 years). If you have any data to contribute please let me know. Gernot