sel4bench icon indicating copy to clipboard operation
sel4bench copied to clipboard

Published 20 hours ago • verified publisher icon seL4

Question about benchmark results

Open ChenYangng opened this issue 11 months ago • 1 comments

Chapter 6 of the seL4 white paper states that the overhead of a round-trip IPC is approximately 720 cycles. Up-to-date performance results listed on the [seL4 Benchmarks page] (https://sel4.systems/About/Performance/) look much better, 382cycles for a IPC call on i7-6700/Skylake.I wonder why.

ChenYangng avatar Feb 28 '24 02:02 ChenYangng

Call is only one side of an IPC. A round-trip is Call+Reply, which at the moment is 383+389=772 cycles.

gernotheiser avatar Feb 28 '24 23:02 gernotheiser