Automated heap sizing in the poly/ML runtime
David R. White, Jeremy Singer, Jonathan M. Aitken, David C. J. Matthews · 2012
Typical theorem-proving workloads on the Poly/ML runtime may execute for several hours, occupying multi-gigabyte heaps. The runtime heap size may be fixed at execution startup time, or it may be allowed to vary dynamically. To date, runtime heap size growth has been implemented using simple hard-coded heuristics. In this position paper, we argue that a mathematically rigorous approach to heap sizing, based on control theory, is more appropriate.