Support a core requirement per run that is different than the core limit

[PhilippWendler]

BenchExec currently supports a core limit per run. Our benchmark definition also allows to specify a core requirement per run, but this is currently undocumented, ignored by BenchExec itself, and only honored by some systems that are used in combination with BenchExec.

The semantics of such a core requirement are: If the core requirement r is higher than the core limit l, then r cores are reserved per run, although the run is allowed to use only l cores. The remaining r-l cores stay unused. If the core requirement r is lower than the core limit l, than each run gets at least r cores and at most l cores depending on how many cores exist (and each parallel run gets the same amount of cores).

In particular, for the first case (r > l) there are some use cases where a less than 100% tight packing of runs onto cores is desired:

• In order to reduce influences between runs due to shared memory bandwidth, L3 cache etc. one could want to run less than the possible number of runs per CPU.
• Benchmarking how a tool scales with different number of cores: If one wants to benchmark a tool with for example a core limit of 1, 2, 4, etc. while keeping the same number of parallel runs in each of these benchmarking instances.

A special case of this is to avoid use of hyper threading, i.e., to keep all but one virtual core per physical core unused, in order to get higher performance. This case was requested in #122 and implemented with --no-hyperthreading.

Currently it is in principle possible for a user to achieve this with --allowedCores, but this would need a manual computation of which cores to exclude and this computation depends on non-obvious details of the hardware architecture.

[PhilippWendler]

An open question is how to pick l cores out of r cores if r > l: One can either pick l cores that are as close to each other as possible (same strategy as if r = l), or pick l cores that maximize usage of available hardware resources like physical cores. In the latter case it could get tricky to support cases where r is not a power-of-two multiple of l.

[PhilippWendler]

from @dbeyer: "my opinion would be to pack tightly such that the performance is the same for r=2, l=2 versus r=4, l=2."

[CGall42]

The option to specify a core requirement is now implemented.
If r > l (the coreRequirement r ist larger than the coreLimit l):
the algorithm reserves r cores per run and at the end slices each list of cores so that it only contains l cores.
If r < l :
the algorithm starts at l cores per run and checks, whether a core distribution works out with the cores available. If not, the number of cores per run is reduced by one until the numbers work out. The algorithm uses the highest possible number of cores per run between r & l .
See also: 8cce256