[seL4] Re: Slowpath IPC mechanism

On 21 Feb 2023, at 08:32, mincheol@vt.edumailto:mincheol@vt.edu wrote:

I am wondering how the slowpath IPC mechanism works. Does it use shared memory to transfer the IPC message?

The kernel copies the data directly from the sender’s to the receiver’s IPC buffer. You should think as IPC as the microkernel equivalent of a system call, and the “payload” are the syscall arguments. It’s not meant for bulk data transfer.

Shared-memory communication can be implemented at user-level, synchronising with Notifications.

Gernot