[isabelle-dev] Poly/ML x86_64_32 available for testing

Fabian Immler immler at in.tum.de
Fri Jan 25 17:40:00 CET 2019


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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190125/42eab9e4/attachment.bin>


More information about the isabelle-dev mailing list