[isabelle-dev] Poly/ML x86_64_32 available for testing
immler at in.tum.de
Fri Jan 25 17:40:00 CET 2019
Great, thanks for looking into this!
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev