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

[Tobias Nipkow]

On 29/10/2017 21:52, Makarius wrote:
> 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.

Very nice indeed!

Tobias

> 
>> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171030/7bdb175c/attachment.bin>