[isabelle-dev] isabelle build
makarius at sketis.net
Wed Aug 8 21:20:10 CEST 2012
On Wed, 8 Aug 2012, David Matthews wrote:
> Actually, one has to be careful when interpreting the parallelism
> figures. Much of the time an ML application is memory-bound which means
> that using more processors can make an improvement in overall run-time
> but the overall CPU usage will grow. As far as I can tell, the time
> that a processor spends waiting for memory counts as its CPU time unlike
> when it is waiting for IO.
The business of multicore programming has indeed its own numerology. The
standard trick is to burn a lot of CPU cycles and then make a good elapsed
time vs. cpu time ratio that is then show as flashy "speedup factor".
This is what the "factor" in Isabelle session timing essentially does,
although it is not completely pointless, because it shows how much of the
CPU resources are actually used.
Concerning the "burning of cycles", here is a comparison with a separate
run with only 2 single-threaded processes:
2:42:10 elapsed time, 6:02:41 cpu time, factor 2.23
The hot one from before with 4 processes * 4 threads was this:
0:45:45 elapsed time, 8:44:02 cpu time, factor 11.45
So we are pretty well off, even on such a hot day where the CPU
temperature of the Mac Pro is usually around 60-80 degree celsius, instead
of the half-idle 30-40 degree.
Since this machine is hyperthreaded, there is another factor that is
difficult to count with. Overloading with many threads causes the CPU
accounting to go up, but it helps a bit in the outcome.
Practically, what matters is the wall-clock time speedup, and maybe the
level of noise that CPU fans are producing.
More information about the isabelle-dev