Makarius wrote: > There was indeed something odd with sharing: David Matthews has changed > that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46).
I may give it another try later... > > Hardware: > > i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD > > > > Common build flags: > > ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2" > > > > Configurations: > > polyml 5.7.1 x86_64 ML_OPTIONS="--maxheap 24G -H 500 > > --gcthreads 6" > > polyml-a444f281ccec x86_64 ML_OPTIONS="--maxheap 24G -H 500 > > --gcthreads 6" > > For this hardware I recommend threads=6. In the sessions beyond HOL, I see a speedup from threads=12. The timings are basically the same with threads=10, but I have not checked the full range of possibilities. I've made sure that the machine is mostly idle; things will be much different if several processes start competing for the ressources. Configurations: threads=6 threads=10 threads=12 Times: Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.12) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished HOL (0:02:21 elapsed time, 0:07:47 cpu time, factor 3.30) Finished HOL (0:02:25 elapsed time, 0:08:56 cpu time, factor 3.68) Finished HOL (0:02:32 elapsed time, 0:09:46 cpu time, factor 3.84) Finished HOL-Lib (0:05:47 elapsed time, 0:25:18 cpu time, factor 4.37) Finished HOL-Lib (0:05:12 elapsed time, 0:32:29 cpu time, factor 6.24) Finished HOL-Lib (0:05:10 elapsed time, 0:35:32 cpu time, factor 6.88) Finished HOL-AFP (0:06:33 elapsed time, 0:27:55 cpu time, factor 4.26) Finished HOL-AFP (0:05:51 elapsed time, 0:34:10 cpu time, factor 5.83) Finished HOL-AFP (0:05:41 elapsed time, 0:35:44 cpu time, factor 6.28) Finished IsaFoR_1 (0:05:11 elapsed time, 0:22:30 cpu time, factor 4.34) Finished IsaFoR_1 (0:05:04 elapsed time, 0:27:15 cpu time, factor 5.38) Finished IsaFoR_1 (0:05:21 elapsed time, 0:29:58 cpu time, factor 5.59) Finished IsaFoR_2 (0:05:57 elapsed time, 0:21:49 cpu time, factor 3.66) Finished IsaFoR_2 (0:05:43 elapsed time, 0:26:24 cpu time, factor 4.61) Finished IsaFoR_2 (0:05:40 elapsed time, 0:27:39 cpu time, factor 4.87) Finished IsaFoR_3 (0:07:13 elapsed time, 0:31:05 cpu time, factor 4.30) Finished IsaFoR_3 (0:06:51 elapsed time, 0:40:15 cpu time, factor 5.87) Finished IsaFoR_3 (0:06:45 elapsed time, 0:43:32 cpu time, factor 6.45) Finished IsaFoR_4 (0:08:37 elapsed time, 0:24:58 cpu time, factor 2.90) Finished IsaFoR_4 (0:08:48 elapsed time, 0:27:08 cpu time, factor 3.08) Finished IsaFoR_4 (0:08:47 elapsed time, 0:27:52 cpu time, factor 3.17) Finished Code (0:08:04 elapsed time, 0:08:12 cpu time, factor 1.02) Finished Code (0:08:00 elapsed time, 0:08:08 cpu time, factor 1.02) Finished Code (0:07:59 elapsed time, 0:08:08 cpu time, factor 1.02) > Moreover note that --gcthreads is automatically provided, if ML_OPTIONS > does not say anything else. I intended to experiment with smaller numbers but have not yet done so. On another, similar machine, --gcthreads=2 was just as fast as 6. Cheers, Bertram _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev