Re: [isabelle] Isabelle2019-RC2 Does poly really honor --maxheap?



On 24/05/2019 01:04, Eugene W. Stark wrote:
> This might not be new to Isabelle2019-RC2, but I thought that I had set a limit
> on the size of the ML heap, but it is still exceeding that and sending my system
> into thrashing mode.

There have been significant changes in Poly/ML in the latest releases,
changing the game each time:

  * Isabelle2019: Poly/ML 5.8
  * Isabelle2018: Poly/ML 5.7
  * Isabelle2017: Poly/ML 5.6

The relevant NEWS entry for Isabelle2019 is:

* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
the full overhead of 64-bit values everywhere. This special x86_64_32
mode provides up to 16GB ML heap, while program code and stacks are
allocated elsewhere. Thus approx. 5 times more memory is available for
applications compared to old x86 mode (which is no longer used by
Isabelle). The switch to the x86_64 CPU architecture also avoids
compatibility problems with Linux and macOS, where 32-bit applications
are gradually phased out.



> Contents of my ~/.isabelle/Isabelle2019-RC2/etc/settings
> 
> ISABELLE_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
> ML_PLATFORM="${ISABELLE_PLATFORM}"
> ML_HOME="${POLYML_HOME}/x86_64-linux"
> ML_OPTIONS="--maxheap 12000"

That setup looks fairly old-fashioned, and is obsolete in Isabelle2019.
The default x86_64_32 platform allows 16GB ML heap, and x86_64 only
makes sense for something like 32-64 GB.

If you remove all these accumulated settings, it should work fine.


> ps output showing poly with --maxheap option applied:
> 
> gene     18897 75.2 71.7 23475004 17680688 ?   Ssl  May21 2365:39
> /opt/Isabelle2019-RC2/contrib/polyml-5.8/x86_64-linux/poly -q --maxheap 12000 --gcthreads 0 --eval
> (PolyML.SaveState.loadHierarchy ["/home/gene/.isabelle/Isabelle2019-RC2/heaps/polyml-5.8_x86_64-linux/Pure",
> 
> Output from "top":
> 
>   PID USER      PR  NI    VIRT    RES    SHR S  %CPU %MEM     TIME+ COMMAND
> 
> 18897 gene      20   0 22.372g 0.016t   6104 S 127.9 71.6   2367:46 poly

I see 16GB resident memory here, which is sufficiently close to the
specified 12GB to hold up the claim that poly manages its memory
correctly: there can be more things outside of the ML heap, e.g.
generated code and stacks.

It is up to David Matthews to explain further details.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.