[seL4] can IPC be concurrent running?

Hi,

We can get the definition of IPCBuffer from here https://github.com/seL4/seL4/blob/master/libsel4/arch_include/arm/sel4/arch/... enum { seL4_GlobalsFrame = 0xffffc000, };

It is fixed in one virtual space, that means the IPC in seL4's thread cann't be concurrent, we can't prepare more than 1 IPC request at the same time, for we call these function: seL4_SetTag, seL4_SetMR, seL4_SetUserData wil use this buffer, but there is no locker to protect the buffer.

Is my understanding correct?

Xilong Pei Tongji University 2015/7/6