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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
