[isabelle-dev] Poly/ML x86_64_32 available for testing

[Bertram Felgenhauer]

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