[isabelle-dev] Slow builds due to excessive heap images
immler at in.tum.de
Fri Nov 3 16:36:35 CET 2017
> Am 03.11.2017 um 14:56 schrieb Fabian Immler <immler at in.tum.de>:
>> Am 02.11.2017 um 18:00 schrieb Makarius <makarius at 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
ML \<open>timeap Check.check (0 upto 7)\<close>
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 4848 bytes
Desc: not available
More information about the isabelle-dev