[isabelle-dev] Multicore performance preview

[Makarius]

Here are some numbers of the next stage of parallelism in Isabelle, where 
both the theory graph structure and the inherent irrelevance of proofs is 
taken into account.  The hardware is a Mac Pro with 4 cores (i.e. 2 plain 
old dual-core Xeons); times are for isabelle usedir -M 4 vs. -M 1 in 
alternating lines:

Finished HOL (0:03:30 elapsed time, 0:06:17 cpu time, factor 1.79)
Finished HOL (0:05:05 elapsed time, 0:05:04 cpu time, factor 0.99)
Finished HOL-Algebra (0:01:36 elapsed time, 0:03:09 cpu time, factor 1.96)
Finished HOL-Algebra (0:02:46 elapsed time, 0:02:44 cpu time, factor 0.98)
Finished HOL-Auth (0:02:11 elapsed time, 0:06:44 cpu time, factor 3.08)
Finished HOL-Auth (0:06:08 elapsed time, 0:06:08 cpu time, factor 1.00)
Finished HOL-Bali (0:02:31 elapsed time, 0:04:12 cpu time, factor 1.66)
Finished HOL-Bali (0:03:39 elapsed time, 0:03:46 cpu time, factor 1.03)
Finished HOL-HoareParallel (0:01:35 elapsed time, 0:04:15 cpu time, factor 2.68)
Finished HOL-HoareParallel (0:03:56 elapsed time, 0:03:57 cpu time, factor 1.00)
Finished HOL-Library (0:01:10 elapsed time, 0:02:55 cpu time, factor 2.50)
Finished HOL-Library (0:02:25 elapsed time, 0:02:29 cpu time, factor 1.02)
Finished HOL-Main (0:01:52 elapsed time, 0:03:10 cpu time, factor 1.69)
Finished HOL-Main (0:02:34 elapsed time, 0:02:34 cpu time, factor 1.00)
Finished HOL-MetisExamples (0:00:17 elapsed time, 0:00:42 cpu time, factor 2.47)
Finished HOL-MetisExamples (0:00:36 elapsed time, 0:00:35 cpu time, factor 0.97)
Finished HOL-MicroJava (0:02:09 elapsed time, 0:05:18 cpu time, factor 2.46)
Finished HOL-MicroJava (0:04:52 elapsed time, 0:04:54 cpu time, factor 1.00)
Finished HOL-Nominal (0:00:21 elapsed time, 0:00:26 cpu time, factor 1.23)
Finished HOL-Nominal (0:00:24 elapsed time, 0:00:22 cpu time, factor 0.91)
Finished HOL-Nominal-Examples (0:05:25 elapsed time, 0:13:42 cpu time, factor 2.52)
Finished HOL-Nominal-Examples (0:11:39 elapsed time, 0:12:31 cpu time, factor 1.07)
Finished HOL-Plain (0:00:53 elapsed time, 0:01:24 cpu time, factor 1.58)
Finished HOL-Plain (0:01:09 elapsed time, 0:01:07 cpu time, factor 0.97)
Finished HOL-SET-Protocol (0:00:51 elapsed time, 0:02:07 cpu time, factor 2.49)
Finished HOL-SET-Protocol (0:01:58 elapsed time, 0:01:58 cpu time, factor 1.00)
Finished HOL-UNITY (0:01:17 elapsed time, 0:02:29 cpu time, factor 1.93)
Finished HOL-UNITY (0:02:11 elapsed time, 0:02:09 cpu time, factor 0.98)
...
0:37:28 elapsed time, 1:17:00 cpu time, factor 2.05
1:06:14 elapsed time, 1:07:10 cpu time, factor 1.01

In order to try it yourself you need to enable the future_scheduler option 
in src/Pure/Concurrent/ROOT.ML; those with 8 core Macs should get slightly 
better numbers.  Does anybody have 12 or 16 cores around?

You will need the latest Poly/ML 5.2.1 version to prevent a strange GC 
deadlock problem in 5.1/5.2.

Apart from that the main reason why the new scheduler is still inactive by 
default are a couple of legacy features in Isabelle/HOL packages. The 
struggle to get rid of legacy stuff will continue ...


	Makarius