Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2023-RC0: ML heap size has been signif...

Email Gateway (Jun 07 2023 at 19:20):

From: Makarius <makarius@sketis.net>
Here are some a notable NEWS items.

* General *

• ML heap usage and stored heap size has been significantly reduced,
  especially for applications with a lot 'locale' or 'class' context
  switches, e.g. "definition (in loc)". The shrink factor is usually in
  the range 1.1 .. 2.0, but a factor 2 .. 25 has been seen as well. This
  often allows big applications to return to the "small" 64_32 memory
  model with its hard limit of 16 GiB, and thus reduce the heap size by
  another factor 1.8.

* ML *

• Improved implementations and signatures of functor Table() and
  corresponding functor Set().

  • Specific Set().T supersedes Table().set = unit table, with concrete
    instances Intset, Symset, Termset etc.

  • Data representation is more compact than before, approx. 85% .. 110%
    of a plain list (e.g. see structure AList or Ord_List, respectively).

  • The new "size" operation works with constant time complexity and
    minimal space overhead: small structures have no size descriptor.

• Operations ML_Heap.sizeof1 and ML_Heap.sizeof determine the object
  size on the heap in bytes. The latter works simultaneously on multiple
  objects, taking implicit sharing of values into account. Examples for
  the default 64_32 platform (4 bytes per machine word):

  val s = "aaaabbbbcccc";
  val a = ML_Heap.sizeof1 s;
  (20: 2 words descriptor + 3 words content)
  val b = ML_Heap.sizeof [s, s];
  (20: shared values without list structure)
  val c = ML_Heap.sizeof1 [s, s];
  (*44 = 20 + 24: shared values + 2 * 3 words per list cons*)

That emerged recently on request of some high-end users with really huge ML
heaps. Many applications in AFP benefit as well, like the Category Theory
sessions by Eugine Stark, e.g. see "stored_heap" in
https://isabelle.sketis.net/devel/build_status/AFP/Category3.csv

The numbers are for batch-builds, i.e. the parent heap hierarchy for a running
Isabelle/PIDE session. I did not make any measurements on the ML heap of the
running PIDE session yet.

(I don't plan to do anything further for the Isabelle2023 release: a factor
1.1 .. 25 is good enough and other things are more pressing.)

Makarius

Last updated: Jan 04 2025 at 20:18 UTC