[isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 28/10/17 22:26, Makarius wrote:
> 
> Overall, performance is mostly the same as in Poly/ML 5.6 from
> Isabelle2017, but there are some dropouts. In particular, loading heap
> images has become relatively slow: this impacts long heap chains like
> HOL-Analysis or big applications in AFP. E.g. see
> http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
> (timing vs. ML timing).
> 
> I've shown this to David Matthews already and await his answer. It could
> be just an accident in Poly/ML 905dae2ebfda or inherent due to the new
> heap + GC management that is more robust against out-of-memory failures.

David Matthews has done a great job to improve this in Poly/ML
e8d82343b692 (see Isabelle/d0f12783cd80). It means that loading of
complex heap hierarchies is now faster than in Poly/ML 5.6.


> Independently of that, excessive use of intermediate heap images makes
> builds much slower than necessary, because multithreading is reduced by
> the structural serialization. Here is a typical example:

Here is an updated test, on different hardware:

Isabelle/d0f12783cd80
AFP/88218011955a

ML_PLATFORM="x86_64-linux"
ML_HOME="/home/makarius/.isabelle/contrib/polyml-test-e8d82343b692/x86_64-linux"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 3000 --maxheap 16000"

$ isabelle build -o threads=6 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.97)
Finished HOL (0:03:48 elapsed time, 0:11:11 cpu time, factor 2.93)
Finished HOL-Library (0:02:05 elapsed time, 0:08:49 cpu time, factor 4.24)
Finished HOL-Computational_Algebra (0:01:05 elapsed time, 0:02:44 cpu
time, factor 2.50)
Finished HOL-Algebra (0:01:44 elapsed time, 0:04:23 cpu time, factor 2.53)
Finished JNF-HOL-Lib (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.58)
Finished JNF-AFP-Lib (0:01:36 elapsed time, 0:06:37 cpu time, factor 4.13)
Finished Jordan_Normal_Form (0:04:47 elapsed time, 0:13:25 cpu time,
factor 2.80)
Finished Subresultants (0:01:01 elapsed time, 0:02:33 cpu time, factor 2.48)
Finished Pre_BZ (0:01:31 elapsed time, 0:05:35 cpu time, factor 3.66)
Finished Berlekamp_Zassenhaus (0:02:29 elapsed time, 0:07:41 cpu time,
factor 3.09)
Finished Pre_Algebraic_Numbers (0:00:32 elapsed time, 0:01:06 cpu time,
factor 2.06)
Finished Algebraic_Numbers_Lib (0:01:25 elapsed time, 0:03:44 cpu time,
factor 2.62)
Finished Linear_Recurrences (0:00:43 elapsed time, 0:01:22 cpu time,
factor 1.88)
Finished Linear_Recurrences_Test (0:02:15 elapsed time, 0:07:49 cpu
time, factor 3.46)
0:26:13 elapsed time, 1:17:50 cpu time, factor 2.97

$ isabelle build -o threads=6 -o timeout_scale=4 -d '$AFP' -f
Linear_Recurrences_Test
Finished Pure (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.97)
Finished HOL (0:03:52 elapsed time, 0:11:22 cpu time, factor 2.93)
Finished Linear_Recurrences_Test (0:12:02 elapsed time, 0:52:56 cpu
time, factor 4.40)
0:16:42 elapsed time, 1:04:38 cpu time, factor 3.87


	Makarius