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