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. > 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. The benchmarks measure cost of IPC 1 way. So in the first case its 2-1. > 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. The comment here is just incorrect and outdated. Cheers, Anna.? ?
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
