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
