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
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