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

[Makarius]

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:

Isabelle/2444c8b85aac
AFP/2eacf2ed7d5d

x86_64_32-linux --minheap 1500 threads=8
Finished HOL-ODE-Numerics (0:17:18 elapsed time, 0:45:28 cpu time,
factor 2.63)
Finished Lorenz_C0 (0:12:06 elapsed time, 1:29:19 cpu time, factor 7.37)

x86_64-linux --minheap 1500 threads=8
Finished HOL-ODE-Numerics (0:19:19 elapsed time, 0:49:46 cpu time,
factor 2.58)
Finished Lorenz_C0 (0:06:54 elapsed time, 0:50:34 cpu time, factor 7.33)


	Makarius