Wrong assumption about number of counters in benchmarks

[JDuchniewicz]

I have been testing RPi4B recently both in AArch64 and AArch32 modes and found out that while for the 64-bit variant sel4bench works fine it fails to pass for 32-bits.

The problem stems from having different numbers of performance counters reported by the PMCR register (0 for 32 and 6 for 64). The places where we implicitly rely on them being greater than 0 are:
In scheduler:
void benchmark_set_prio_average(ccnt_t results[N_RUNS][NUM_AVERAGE_EVENTS], seL4_CPtr auth)
and void benchmark_yield_average(ccnt_t results[N_RUNS][NUM_AVERAGE_EVENTS]).
In signal: void high_prio_signal_fn(int argc, char **argv)

Whereas in the scheduler there is an assert that fires, in the two other places we pass the 0 as the divisor to the DIV_ROUND_UP function that returns 1 from the division (due to an UB?).

The docs quote:

Indicates the number of event counters implemented. This value is in the range of 0b00000-0b11111. If the value is 0b00000, then only PMCCNTR is implemented. If the value is 0b11111, then PMCCNTR and 31 event counters are implemented.

Maybe we can rely on this value being 0 and the asserts are unnecessary?

[JDuchniewicz]

Ad: DIV_ROUND_UP: Raspberry Pi 4B is Cortex-A72 which is ARMv8 architecture and when dividing by 0 we get 0:

So it's not UB.

[lsf37]

It's still UB in C, though, so the compiler could decide to specifically do whatever. Unlikely that it will, but it would be allowed.

So if we want to allow 0, we should explicitly check for it and return our own 0.

[Indanz]

But how does PMCCNTR compare to the other event counters? Is it regular, or is it totally different?

If it's regular, then the simple fix is to let sel4bench_get_num_counters() return SEL4BENCH_ARMV7A_PMCR_N(sel4bench_private_read_pmcr()) + 1;, because that's what the register implements: Effectively a count from 1 to 32, encoded as 0-31.

[JDuchniewicz]

PMCCNTR is counting per cycle (if we don't configure any divisors) so it can do the job. With this changed, I got the RPi4B to pass sel4bench:
seL4/seL4_libs@8c2d5a7

[Indanz]

Good, sanity restored. Please open a pull request.