Re: [isabelle] 32 vs. 64 bit

On 03/02/2016 10:31, Lars Hupel wrote:
I don't have a deep knowledge of the
Poly/ML implementation but my understanding is that, while the 64-bit
version uses more memory to accomplish the same
thing, you *must* use it if you want to use more than N bytes of RAM
(for some N; 4GB?).

As far as I understand it, the 32 bit reduces heap requirements in the
first place. Also, it gives better performance. For example, AODV with
threads=8 takes 1h39m on 64 bit, but just 1h20m on 32 bit.*

As an interesting side note: I've found that under low memory pressure,
that session may reserve north of 50 GB memory (using 64 bit), but it is
also fine to run with less than 4 GB (using 32 bit). My initial
suspicion that 64 bit might be faster for huge sessions by reducing GC
time turned out to be false.

Typically 64-bit mode takes around twice as much memory as 32-bit. Most of the data is things like cons-cells that are twice as big.

I suspect that your application has a great deal of shareable data in it. When memory is tight the Poly/ML GC runs a sharing pass that looks for common data and uses that to reduce the size of the live data. It's expensive to run and the results are only known when the run is complete so it is only used when absolutely necessary. In 32-bit mode the heap size is limited by the system to somewhere around 3.5G so it's much more likely to run the sharing pass there than with a larger available heap in 64-bit mode. It may well be that in your particular case the heap can be reduced quite substantially. I seem to recall that NinjaThreads the first time the sharing pass was run it achieved somewhere around an 80% reduction.

It could be worth trying your example in 64-bit mode but limiting the heap with --maxheap to say 8G. Maybe there ought to be a way to tell the heap sizer that this application may benefit from running the sharing pass sooner rather than later.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.