I believe CPU IDs are not guaranteed to be contiguous and mp_maxid is what should be used instead

In light of D41319 and the issues of what was observed when similar was done there. Presently this is untested, but I'm reasonably sure this is correct.

I'm not marking this as a parent of D41319 since there isn't a strict ordering requirement. Just D41319 may make the IPI counters become unpleasantly large overhead. Similar to the issues observed before D36838.

In D41462#944302, @emaste wrote:

I believe CPU IDs are not guaranteed to be contiguous and mp_maxid is what should be used instead

I'm fairly sure they are on ARM and the other INTRNG platforms, but you could be right (reviewers, you know this better than I!). I'm not actually finding any documentation on what the differences between all the *mp_* variables are. I can roughly guess most of them, but the difference between mp_ncpus and smp_cpus isn't showing up.

Yes, I suspect that CPU IDs are contiguous on platforms which use intrng, but machine independent code should nonetheless use the range [0, mp_maxid] to index CPUs. See CPU_FOREACH(), for instance.

but the difference between mp_ncpus and smp_cpus isn't showing up.

mp_ncpus is the number of CPUs enumerated using platform-specific interfaces, smp_cpus is the number of CPUs that have been initialized and have started running kernel code. Once the kernel finishes booting, these two numbers are typically equal. There might be rare cases where they are not because one or more APs failed to initialize, and the kernel is limping along anyway.

The range is [0, mp_maxid], not [0, mp_maxid), so we should allocate mp_maxid + 1 counters.

Booted in QEMU on Cirrus-CI https://cirrus-ci.com/task/6483512983814144