[josephg]

> I thought newer microkernels... Reduced that? Fixed it? I forget, I just had the impression it wasn't actually that bad

SeL4 is a microkernel like this. They’ve apparently aggressively optimized IPC far more than Linux ever has. Sending a message via sel4 ipc is apparently an order of magnitude or two faster than syscalls under Linux. I wouldn’t be surprised if most programs performed better under sel4 than they do under Linux - but I’d love to know for real.

[winternewt]

The trick with L4 is they treat IPC basically like syscalls. Arguments are left on CPU registers instead of serializing them to a message buffer. The only significant work performed is a change of virtual memory map. The called process continues execution within the time slice of the caller, instead of waiting for the thread scheduler or using synchronization primitives. While some of this could possibly be achieved with Linux, a lot of the optimization is ingrained into the calling convention and so would require changes to the user-mode source code.

[pas]

so simple recompilation can speed things up? sounds amazing. (but of course, can it?) also, it sounds a bit like restartable sequences (from Google).