makarius at sketis.net
Tue Dec 23 21:43:04 CET 2008
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:
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.
The magic parameters for the above measurements are:
ISABELLE_USEDIR_OPTIONS="-i false -d false -M max"
ML_OPTIONS="--immutable 800 --mutable 1200"
More information about the isabelle-dev