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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev