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

[David Matthews]

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