Hi, I attached two of the benchmark results that I pulled from the last run.
Looking at the top of each of them I get similar results to you: "Benchmark": "One way IPC microbenchmarks", "Direction": "client->server", "Function": "seL4_Call", SMP on (mean, stddev) 444.125, 5.176871642217914 SMP off (mean, stddev) 305.125, 8.94427190999916 The thing to note is that the measurement is still IPC between two threads of the same address space on the same core. The overhead comes from a lock that is introduced in the SMP seL4 configuration. When any syscall happens, the core that the syscall is performed on has to acquire the lock before it can handle the syscall. If another core is performing a syscall, the first core will be blocked until the lock is released. This can be found in the kernel entry code "kernel/src/arch/arm/c_traps.c", look at the NODE_LOCK_SYS macro. Essentially the overhead comes from the memory barrier required to implement the lock, and the extra instructions for acquiring and releasing the lock on every syscall. Kind regards, Kent.
sabre-aarch32.json
Description: sabre-aarch32.json
sabre-aarch32-smp.json
Description: sabre-aarch32-smp.json
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
