HI, I have a question about sel4bench IPC.
Thanks for the reply.

1. Making seL4_IPCBuffer and mapping into the thread is necessary? 
I think that sending short messages don't need seL4_IPCBuffer, is it right?

2. This is seL4_Call annotation in benchmark_param.
/* Call fastpath between client and server in the different address space */

But I can't understand how to measure seL4_Call function performance.  

[Client thread]                          [Server thread]
seL4_Call                                 seL4_ReplyRecv(I'm not sure)

1) client send message.
2) server receive message.
3) server send message.
4) client receive message. 

seL4_Call performance in sel4bench excluding overhead , is it right? = 1) + 2)  + 3) + 4) - 3) - 4)

3. This is seL4_Send annotation in benchmark_param.
/* Send slowpath (no fastpath for send) same prio client-server, different address space */
But client_prio(seL4_MaxPrio - 1) and server_prio(seL4_MaxPrio - 2) is different.