[isabelle-dev] NEWS

[Makarius]

On Tue, 23 Dec 2008, Makarius wrote:

> * Proofs of fully specified statements are run in parallel on multi-core 
>   systems.  A speedup factor of 2-3 can be expected on a regular 4-core 
>   machine, if the initial heap space is made reasonably large (cf. Poly/ML 
>   option -H).  [Poly/ML 5.2.1 or later]

See also http://isabelle.in.tum.de/devel/stats/at-mac-poly-5.1-para.html 
for some real numbers.  Getting actual performance out of parallelims is a 
very hard business.  Nonetheless, two sessions look quite promising:

  http://isabelle.in.tum.de/devel/stats/at-mac-poly-5.1-para/HOL.png
  http://isabelle.in.tum.de/devel/stats/at-mac-poly-5.1-para/HOL-Nominal-Examples.png

The reason for quite good performance of "HOL" is that with full proof 
terms, the overhead for scheduling proofs is negligible compared to 
crunching of huge proof objects.  Writing the final image eats up some 
time again -- 2 GB heap need to be compressed to a 100 MB image (by 
maximal data sharing).

The reason for the impressive speedup of "HOL-Nominal" is that the 
monolithic Class.thy is now parallelized at the level of proofs.


If anybody has > 4 cores, or >= 4 cores and >= 16 GB memory, I would be 
interested to see your numbers.  Note that the speedup factor can be 
influenced by fine-tuning heap options of Poly/ML: -H or --immutable vs. 
--mutable.


The magic parameters for the above measurements are:

  ISABELLE_USEDIR_OPTIONS="-i false -d false -M max"
  HOL_USEDIR_OPTIONS="-p 2"

  ML_OPTIONS="--immutable 800 --mutable 1200"


	Makarius