Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 32 vs. 64 bit


view this post on Zulip Email Gateway (Aug 22 2022 at 12:46):

From: Lars Hupel <hupel@in.tum.de>
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.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 12:47):

From: David Matthews <dm@prolingua.co.uk>
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.

David


Last updated: Apr 20 2024 at 12:26 UTC