I looked at it once more: profiling told me that IntInf.pow (in combination with Par_List.map) seems to be the culprit.
The following snippet shows similar behavior: ML ‹ fun powers  =  | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs; Par_List.map (fn i => powers (i upto 100000 * i)) (0 upto 31) › polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02 polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu time, factor 5.70 polyml-5.6-1/x86_64-darwin: 0.570s elapsed time, 1.748s cpu time, 0.000s GC time polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu time, 42.602s GC time > Am 03.11.2017 um 16:36 schrieb Fabian Immler <imm...@in.tum.de>: > > > >> Am 03.11.2017 um 14:56 schrieb Fabian Immler <imm...@in.tum.de>: >> >> >>> Am 02.11.2017 um 18:00 schrieb Makarius <makar...@sketis.net>: >>> >>> I am more worried about the factor 5 performance loss of Lorenz_C0: now >>> (3:26:41 elapsed time, 16:49:16 cpu time, factor 4.88). It is unclear if >>> the problem is related to Flyspeck-Tame. I did not approach it yet, >>> because the HOL-ODE tower is really huge. >>> >>> It would greatly help to see the problem in isolated spots. I usually >>> send David specimens produced by code_runtime_trace. >> At least on my Mac, there seems to be a problem with (or induced by) >> parallelism: >> The attached check.sml is the code extracted from Lorenz_C0. >> "Check.check xs" does a Par_List.forall on the list xs and Par_list.map in >> the computation for individual elements. >> >> With isabelle/fc87d3becd69 and polyml-test-e8d82343b692/x86_64-darwin, >> something goes very wrong: a slowdown by a factor of more than 50, compared >> to Isabelle2017 . >> >> This seems to be related to parallelism: >> In check_seq.sml, I replaced Par_List.forall/Par_list.map with list_all/map. >> In this case isabelle/fc87d3becd69 behaves more or less like Isabelle2017. >> >> I also tried isabelle/fc87d3becd69 with polyml-5.6-1/x86_64-darwin: this >> behaves for both parallel and sequential computations like Isabelle2017. >> >> Unfortunately, I failed to reproduce this behavior on Linux. > > I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap > 1600 --maxheap 4000" if that is relevant). > Invoked with "isabelle build -d . -othreads=8" for the theory below. > > polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu > time, factor 6.94) > polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor > 4.70) > > Both are in isabelle/123670d1cff3 > > -- > > theory Check > imports Pure > begin > > ML_file \<open>check.sml\<close> > ML \<open>timeap Check.check (0 upto 7)\<close> > > end > > > _______________________________________________ > 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