Email Gateway (Nov 24 2021 at 08:27): Email Gateway (Nov 24 2021 at 08:27):From: Lars Hupel <lars.hupel@innoq.com>
Dear list,
I'm porting a small but substantial application (~ 7kLOC, but no custom
tactics or commands) to Isabelle2021-1.
I noticed during regular development with Isabelle/jEdit that Poly/ML
quite aggressively allocates memory. I have a quad-core machine with 24
GB of memory, and it is not uncommon for me to see heap sizes > 10 GB.
Normally, that wouldn't be a problem, however the GC/ML cleanup can take
a long time, during which my entire laptop freezes (unless the OOM
killer chimes in). Just now I saw a GC phase that took ~50 seconds with
an ML heap size of 2 GB.
Cheers
Lars
Email Gateway (Nov 24 2021 at 13:58):From: Lars Hupel <lars.hupel@innoq.com>
After a bit more use, I noticed another strange pattern. Poly/ML
accumulates heap very quickly, but if I manually run
PIDE.session.protocol_command("ML_Heap.full_gc")
in the Console dockable, thus forcing a GC run, it completes within a
few seconds (as expected).
Curiously enough, when an automatic GC run happens, Poly/ML does not
appear to release memory back to the OS, but running the above command does.
Email Gateway (Nov 26 2021 at 11:52):From: Lars Hupel <lars.hupel@innoq.com>
What is your OS version?
Arch, approximately kernel 5.15
Can you can try this with other versions of Poly/ML? Here are some formal
component names:
I haven't had a chance yet but it turns out that setting --max-heap to
4G allows me to work without interruption. I will try other Poly/ML next.
Email Gateway (Nov 26 2021 at 22:17):From: Dominique Unruh <unruh@ut.ee>
I haven't had a chance yet but it turns out that setting --max-heap to
4G allows me to work without interruption. I will try other Poly/ML next.
I have tried to build HOL-Analysis on a 4GB Mac and it completely failed
(i.e., did not finish within a day or two, probably stuck due to
constant swapping). Setting --max-heap to 2G made it work in a few hours
(it was an old system). So it seems that the polyml defaults do not
necessarily use the machine optimally. Maybe you had a similar
situation, just scaled up by a factor of two.
Best wishes,
Dominique.
Email Gateway (Nov 28 2021 at 12:50):From: Lars Hupel <lars.hupel@innoq.com>
The question: Is this really a new problem for Isabelle2021-1 that was absent
in Isabelle2021?
Yes, this problem is new. As I said, I've ported the application to
Isabelle2021-1 and never experienced that kind of excessive heap usage
before.
Email Gateway (Nov 29 2021 at 08:58):From: Lars Hupel <lars.hupel@innoq.com>
They seem to behave differently:
polyml-5.8.2 has smaller heap requirements and frequently runs fast GC
phases.
polyml-test-f86ae3dc1686 appears to also not demand a large heap, but
I've observed long-running GC pauses (similar to the ones I've described
in my original mail)
I tried loading the same theories in the same way to test the hypothesis.
Email Gateway (Nov 29 2021 at 16:14):From: Lars Hupel <lars.hupel@innoq.com>
We need some tangible empirical results to proceed.
I also tried out RC4 and the problem became much worse. I've seen GC
pauses exceeding a minute or more, both with --maxheap 2G and --maxheap 4G.
My laptop has 24G RAM, so theoretically I could increase --maxheap, but
I don't see how that could help if GC pauses grow with more memory.
Email Gateway (Nov 29 2021 at 16:29):From: Manuel Eberl <manuel@pruvisto.org>
Someone on Zulip had a similar problem today, both with Isabelle 2020
and with Isabelle 2021, that we eventually tracked down to "auto
quickcheck": there was a goal that involved "2 ^ 129 :: nat", which
causes auto quickcheck to try to evaluate "2 ^ 129" in successor
arithmetic and leads to horrific memory consumption and freezing.
Since you also only spoke of the problem appearing in Isabelle/jEdit (if
I see correctly), I do wonder: does it also happen if you switch off
auto quickcheck in the settings?
Manuel
Email Gateway (Nov 29 2021 at 16:32):From: Lars Hupel <lars.hupel@innoq.com>
I just checked that out and indeed it does not when disabling Auto
Quickcheck. I also tried running the "quickcheck" command and could
confirm that it is the culprit.
However, I wonder why I never stumbled upon that problem before, given
that this definition appears in my code (and has been for a long time):
definition max_value :: ‹nat› where
‹max_value = 2147483647›
Email Gateway (Nov 29 2021 at 16:38):From: Manuel Eberl <manuel@pruvisto.org>
It really is quite odd. I can never remember having run into problems
like this.
My guess is that some piece of code is supposed to kill auto quickcheck
quickly when it does not find a result (and/or consumes to much memory)
and that this fails under certain circumstances, and perhaps these
circumstances have become more frequent recently.
In any case, the credit belongs to Matthew Torrence. He came up with the
minimal (non-)working example and also figured out that it might have
something to do with auto quickcheck:
https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/ML.20cleanup.20problems
He was going to post about it on the mailing list soon.
Manuel
Email Gateway (Nov 29 2021 at 16:48):From: Manuel Eberl <manuel@pruvisto.org>
Addendum: If one imports HOL-Library.Code_Target_Numeral, this problem
(unsurprisingly) does not happen.
But what is perhaps surprising (at least to me) is that if one then
quickchecks a theorem involving the term "replicate (2^32) True", this
does not lead to the same behaviour (consuming tonnes of memory, whole
system becomes unresponsive) but rather fails very quickly, with the
"quickcheck" command being highlighted with a red background in
Isabelle/jEdit.
It is a complete mystery to me why successor-arithmetic natural numbers
behave so differently from lists. And why the natural-number example
does not also simply crash due to out-of-memory very quickly.
But perhaps these observations will at least allow the rest of you to
pin down what is going on better.
On a related note, I also recall an unresolved post by myself from a few
years ago where I found that running the "approximate" command/tactic on
certain pathological terms. The numbers involved become so huge that
trying to run the command/tactic took down the entire system. (I
couldn't find the thread anymore though)
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-March/msg00008.html
Manuel
Email Gateway (Nov 29 2021 at 17:51):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Some additional comments that might or might not be helpful...
I have been running for some months now on a system with 128GB RAM, with the following settings:
Last updated: Apr 16 2024 at 20:15 UTC