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

[Fabian Immler]

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 <immler at in.tum.de>:
> 
> 
> 
>> 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
> 
> --
> 
> 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-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: 4848 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171103/2528223b/attachment.bin>