You can't really draw conclusions about systems built on Linux vs seL4 from that though. You can have far more IPC in order to do anything useful in microkernels. I'm not dismissing either OS or architecture, but just saying that extrapolating from micro-metrics is very hard when their use in the different architectures varies significantly.