[isabelle-dev] isabelle build timing

[Makarius]

On 04/09/17 13:18, Lars Hupel wrote:
>> The canonical build parameters for this machine appear to be:
>>
>>   isabelle build -j8 -o threads=6
> 
> I find this combination (8*6 = 48 threads) to be surprising, given that
> that machine has only access to 22 physical (non-HT) cores. Judging from
> your list below, this is the minimum number of threads you tried out
> (for distribution only).
Here are more results for Isabelle/19bf4d5966dc and

  ML_PLATFORM="x86-linux"
  ML_HOME="/home/isabelle/contrib/polyml-5.6-1/x86-linux"
  ML_SYSTEM="polyml-5.6"
  ML_OPTIONS="--minheap 1600"

isabelle build -j4 -o threads=8 -a
0:21:09 elapsed time, 4:38:17 cpu time, factor 13.16

isabelle build -j8 -o threads=4 -a
0:17:29 elapsed time, 4:17:50 cpu time, factor 14.74
0:17:25 elapsed time, 4:16:41 cpu time, factor 14.73

isabelle build -j8 -o threads=6 -a
0:16:16 elapsed time, 4:18:04 cpu time, factor 15.86

isabelle build -j6 -o threads=6 -a
0:16:45 elapsed time, 4:22:14 cpu time, factor 15.65


So empirically 8 * 6 comes out best: that is normal multicore
numerology. It can probably be explained by looking in further detail in
which order the sessions are built, and where are wait-times with unused
CPU cores.


	Makarius