On 03/11/2017 19:07, Makarius wrote:
On 03/11/17 19:26, Fabian Immler wrote:
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
I have discovered the same and have now pushed a workaround:
http://isabelle.in.tum.de/repos/isabelle/rev/17eb23e43630
Somehow the IntInf.pow implementation in Poly/ML e8d82343b692 is a bit
wasteful, maybe during the bit vector operation instead of our
IntInf.divMod (_, 2) used here: see
http://isabelle.in.tum.de/repos/isabelle/annotate/17eb23e43630/src/Pure/General/integer.ML#l43
I've had a look at this and pushed a change to IntInf.pow to Poly/ML
master (c2a2961). It now uses Word.andb rather than IntInf.andb which
avoids a call into the run-time system (RTS).
However, this code hadn't changed since 5.6 and when I tested it using
List.map with 5.6 and 5.7.1 I didn't notice much difference; certainly
not the massive differences you found with Par_List.map. The only thing
I can think of is that there were so many calls into the RTS that there
was some contention on a mutex and that was causing problems.
Anyway, try the new version and let me know the results.
David
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
