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.
Hi,
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?
Correct. There is a constant defined for each architecture in libsel4 (`seL4_FastMessageRegisters`) which specifies the size of message that can fit into registers.
The benchmarks measure cost of IPC 1 way. So in the first case its 2-1.
The comment here is just incorrect and outdated. Cheers, Anna.? ?
participants (2)
-
Anna.Lyons@data61.csiro.au
-
송대영