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