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

[Bertram Felgenhauer]

Bertram Felgenhauer wrote:
> Makarius wrote:
> > So this is the right time for further testing of applications:
> > Isabelle2018 should work as well, but I have not done any testing beyond
> > "isabelle build -g main" -- Isabelle development only moves forward in
> > one direction on a single branch.
>
> I have tried this with Isabelle2018 and IsaFoR; I've encountered no
> problems and there's a nice speedup (estimated 1.25 times faster).
> Heap images are 40% smaller, which is a welcome change as well.

I have gathered some more data (below). There are some curiosities:

- Code export (that's the only thing that the 'Code' session does,
  besides theory merges) seems to be slower with polyml-a444f281ccec
  compared to polyml 5.7.1, even when sticking to the x86_64 platform.

- A similar slowdown seems to affect the IsaFoR_3 session, but I don't
  know what's special about that one.

- While most heap images are about 40% smaller with x86_64_32, this is
  not always the case; some heap images ended up being even larger in
  this experiment. Could there be a problem with the sharing pass on
  x86_64_32?

Cheers,

Bertram

Hardware:
  i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD

Software:
  GNU/Linux
  Isabelle2018
  afp-2018 @ 400c722462b3
  IsaFoR @ acb9096ce08a

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"
  polyml-0a6ebca445fc x86_64_32 ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6"
  polyml-a444f281ccec x86_64_32 ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6"

Timings:
  Finished Pure (0:00:11 elapsed time, 0:00:14 cpu time, factor 1.20)
  Finished Pure (0:00:15 elapsed time, 0:00:17 cpu time, factor 1.18)
  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.13)

  Finished HOL (0:02:46 elapsed time, 0:10:50 cpu time, factor 3.91)
  Finished HOL (0:02:41 elapsed time, 0:10:05 cpu time, factor 3.75)
  Finished HOL (0:02:32 elapsed time, 0:09:46 cpu time, factor 3.84)
  Finished HOL (0:02:28 elapsed time, 0:09:20 cpu time, factor 3.78)

  Finished HOL-Lib (0:05:00 elapsed time, 0:35:54 cpu time, factor 7.18)
  Finished HOL-Lib (0:05:19 elapsed time, 0:36:41 cpu time, factor 6.88)
  Finished HOL-Lib (0:05:10 elapsed time, 0:35:32 cpu time, factor 6.88)
  Finished HOL-Lib (0:04:57 elapsed time, 0:34:16 cpu time, factor 6.91)

  Finished HOL-AFP (0:05:59 elapsed time, 0:37:39 cpu time, factor 6.28)
  Finished HOL-AFP (0:06:15 elapsed time, 0:38:31 cpu time, factor 6.15)
  Finished HOL-AFP (0:05:41 elapsed time, 0:35:44 cpu time, factor 6.28)
  Finished HOL-AFP (0:05:33 elapsed time, 0:35:01 cpu time, factor 6.30)

  Finished IsaFoR_1 (0:05:46 elapsed time, 0:31:43 cpu time, factor 5.49)
  Finished IsaFoR_1 (0:05:42 elapsed time, 0:31:06 cpu time, factor 5.46)
  Finished IsaFoR_1 (0:05:21 elapsed time, 0:29:58 cpu time, factor 5.59)
  Finished IsaFoR_1 (0:05:17 elapsed time, 0:29:15 cpu time, factor 5.54)

  Finished IsaFoR_2 (0:06:07 elapsed time, 0:29:37 cpu time, factor 4.84)
  Finished IsaFoR_2 (0:06:04 elapsed time, 0:29:15 cpu time, factor 4.82)
  Finished IsaFoR_2 (0:05:40 elapsed time, 0:27:39 cpu time, factor 4.87)
  Finished IsaFoR_2 (0:05:59 elapsed time, 0:28:14 cpu time, factor 4.72)

  Finished IsaFoR_3 (0:07:30 elapsed time, 0:47:56 cpu time, factor 6.38)
  Finished IsaFoR_3 (0:09:58 elapsed time, 0:55:27 cpu time, factor 5.56) ?
  Finished IsaFoR_3 (0:06:45 elapsed time, 0:43:32 cpu time, factor 6.45)
  Finished IsaFoR_3 (0:06:49 elapsed time, 0:43:20 cpu time, factor 6.35)

  Finished IsaFoR_4 (0:09:40 elapsed time, 0:30:25 cpu time, factor 3.15)
  Finished IsaFoR_4 (0:09:14 elapsed time, 0:29:16 cpu time, factor 3.17)
  Finished IsaFoR_4 (0:08:47 elapsed time, 0:27:52 cpu time, factor 3.17)
  Finished IsaFoR_4 (0:08:52 elapsed time, 0:27:57 cpu time, factor 3.15)

  Finished Code (0:05:30 elapsed time, 0:05:42 cpu time, factor 1.03)
  Finished Code (0:08:34 elapsed time, 0:08:46 cpu time, factor 1.02) ?
  Finished Code (0:07:59 elapsed time, 0:08:08 cpu time, factor 1.02)
  Finished Code (0:08:00 elapsed time, 0:08:08 cpu time, factor 1.02)

  total 00:48:29
  total 00:54:02
  total 00:48:08
  total 00:48:08

Heap image sizes (factor):
   28081037 Pure (1.00)
   25131549 Pure (0.89)
   19271077 Pure (0.68)
   19270685 Pure (0.68)

  410972244 HOL (1.00)
  403934084 HOL (0.98)
  249583659 HOL (0.61)
  249808871 HOL (0.61)

  525949867 HOL-Lib (1.00)
  526132427 HOL-Lib (1.00)
  308088218 HOL-Lib (0.59)
  307456194 HOL-Lib (0.58)

  913422879 HOL-AFP (1.00)
  915450415 HOL-AFP (1.00)
  537947934 HOL-AFP (0.59)
  538445922 HOL-AFP (0.59)

  724672759 IsaFoR_1 (1.00)
  724822231 IsaFoR_1 (1.00)
  428960922 IsaFoR_1 (0.59)
  429004970 IsaFoR_1 (0.59)

  623083120 IsaFoR_2 (1.00)
  623291272 IsaFoR_2 (1.00)
  367497971 IsaFoR_2 (0.59)
  884213127 IsaFoR_2 (1.42) ?

  712211696 IsaFoR_3 (1.00)
  713133672 IsaFoR_3 (1.00)
  419978203 IsaFoR_3 (0.59)
  521702015 IsaFoR_3 (0.73)

  480209352 IsaFoR_4 (1.00)
  481036688 IsaFoR_4 (1.00)
  730273567 IsaFoR_4 (1.52) ?
  745333063 IsaFoR_4 (1.55) ?