NEWS: Poly/ML 64_32 heap size 32 GiB instead of 16 GiB
Makarius
makarius at sketis.net
Tue Jul 14 23:27:33 CEST 2026
*** System ***
* Poly/ML 5.9.2 has been patched to support larger heap size in the
special x86_64_32/arm64_32 mode with 32-bit values: the limit is now 32
GiB, instead of 16 GiB before. The cost is a factor of 1.2 .. 1.5 more
memory requirement (due to alignment of values), and a slowdown factor
0.9 .. 0.95 for average sessions. For very large sessions, the gain is a
speedup factor 1.9 .. 1.2, due to reduced GC time. It also avoids the
need for bulky x86_64/arm64 mode with 64-bit values and excessive GC
time.
This refers to Isabelle/e3c3e01d3eb1.
This is the result of significant work by David Matthews in collaboration with
Martin Desharnais-Schäfer.
The plan is to use the enlarged 64_32 memory model as "one size fits for
almost all applications", and omit the old 64_32 mode with 16 GiB that is in
principle still supported by Poly/ML.
The full 64-bit mode is available as before, but discouraged. Its known GC
performance problems will be addressed at a later stage. (Not now and not for
this release.)
Makarius
More information about the isabelle-dev
mailing list