[isabelle-dev] isabelle build

[Makarius]

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.


 	Makarius