I think elaborate IPC designs are too much trouble, and I favor seL4's "context switch with benefits" approach of delegating larger messages to shared memory. It avoids performance and security hiccups with copying or kernel-mediated shared memory, like in EROS. To be fair, I'm less focused on efficiency and more on simplicity/robustness of the kernel, similar to seL4. Could you elaborate on your thoughts in the IPC space?