On 23/01/2019 12:05, David Matthews wrote:
>
> I've had a look at this under Windows and the problem seems to be with
> calls to IntInf.divMod from generated code, not from IntInf.pow. The
> underlying RTS call used by IntInf.quotRem has changed in the 32-in-64
> version. It previously returned the pair of values by passing in a
> stack location and having the RTS update this. That isn't possible in
> the 32-in-64 version so now it allocates a pair on the heap. For
> simplicity this is now used for the native code versions as well. From
> what I can tell nearly all the threads are waiting for mutexes and I
> suspect that the extra heap allocation in IntInf.quotRem is causing some
> of the problem. Waiting for a contended mutex can cost a significant
> amount of processor time both in busy-waiting and in kernel calls.
>
> I'm not sure what to suggest except not to use concurrency here. There
> doesn't seem to be a way to avoid allocating a pair in IntInf.quotRem.
In the meantime David has produced Poly/ML a444f281ccec and I can
confirm that it works very well:
Isabelle/2444c8b85aac
AFP/2eacf2ed7d5d
x86_64_32-linux --minheap 1500 threads=8
Finished HOL-ODE-Numerics (0:17:18 elapsed time, 0:45:28 cpu time,
factor 2.63)
Finished Lorenz_C0 (0:12:06 elapsed time, 1:29:19 cpu time, factor 7.37)
x86_64-linux --minheap 1500 threads=8
Finished HOL-ODE-Numerics (0:19:19 elapsed time, 0:49:46 cpu time,
factor 2.58)
Finished Lorenz_C0 (0:06:54 elapsed time, 0:50:34 cpu time, factor 7.33)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
