Hello everyone,
I’m trying to benchmark userspace applications in seL4 on a Zynq 7000 board.
I’ve seen some tools are provided in the kernel, sel4bench and platsupport to achieve this, but it seems the clock counters provided are limited to 32 bits.
Therefore when I benchmark long running applications, the counter values I get are not accurate.
I guess my approach is wrong and I was wondering which tools you woud use for this kind of benchmark.
There’s usually a platform specific way to receive an interrupt when performance counters overflow so that a benchmarking runtime can provide a software implementation of a 64 bit counter. But libsel4bench doesn’t support long running benchmarks that require handling overflows: seL4_libs/sel4bench.h at 12.1.x-compatible · seL4/seL4_libs · GitHub
Thank you for your answer !
Note that on 64 bit architectures ccnt_t from sel4bench can be 64-bit of the platform cycle counter exists that is that size.
Mostly since they are unsigned counters we rely on measurements not being so large that an overflow is not a problem - e.g what you benchmark is smaller than the possible overflow time for the counter, so you can get away with normal unsigned arithmetic.
If the counter is going to overflow, you are likely bench-marking something that needs to use a real source of time, not the cycle counter.
I get the idea of how I can manage to do that.
Thank you !