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