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

David Matthews dm at prolingua.co.uk
Wed Jan 23 22:24:43 CET 2019

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.


More information about the isabelle-dev mailing list