Great, thanks for looking into this! Fabian On 1/23/2019 4:24 PM, David Matthews wrote:
On 23/01/2019 21:08, Makarius wrote: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:I had another look and it was a mutex contention problem, just not exactly where I'd thought. Most calls to the run-time system involved taking a lock for a very short period in order to get the thread's C++ data structure. This wasn't a problem in the vast majority of cases but this example involves very many calls to the long-format arbitrary precision package. That resulted in contention on the lock. I've changed this so the lock is no longer needed and it seems to have solved the problem.David
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev