Email Gateway (Aug 22 2022 at 09:11): Email Gateway (Aug 22 2022 at 09:11):From: "Eugene W. Stark" <stark@cs.stonybrook.edu>
Since there is a thread going about various kinds of hanging, I would
like to ask about behavior that I have experienced (with Isabelle2014).
Basically the symptom is that the prover becomes unresponsive, though JEdit
does still respond. Often, the entire buffer becomes highlighted in pink,
and many times it is impossible to continue without exiting JEdit
(thereby exiting the prover) and restarting. While in the stuck state,
the prover (Poly process) exhibits constant CPU consumption. It does not
appear to be a thrashing issue because the disk traffic is low and CPU
utilization high.
I have only rarely seen this problem on my home system, which is a year-old
i5 processor with four cores (I am running Ubuntu 14.04 LTS) and 8GB RAM.
However, it occurs much more often on my office machine, which is a venerable
32-bit, one-core system with 2GB (also running Ubuntu 14.04 LTS).
In fact, it is pretty much impossible to use "try" on that machine because
it almost always results in a stuck prover. Once the situation has arisen,
attempting to delete the "try" from the JEdit buffer does not successfully
cancel the ongoing proof attempt.
I would be interested to know what I should be looking for in order to try
to solve this. When I noticed it this morning on my home system, it appeared
to be because there were several threads occupied by various proof attempts
(I think "blast") that did not terminate. In this particular case I was
able to recover by erasing the "by blast" lines, but when things are truly
stuck (especially on the one-core system) this does not help.
Another situation I have gotten into that produced similar symptoms is when
I inadvertently created recursive simplifier rules. However, I don't think
this is usually the issue.
My question is: is it supposed to be possible for prover threads to hang
around indefinitely (purple mark in right margin and proof method highlighted
in purple) without timing out in some reasonable period? If so, why,
and what should I look for to try to fix the problem? If not, then this would
seem to be an issue that should be looked into.
Thanks for the help.
- Gene Stark
Email Gateway (Aug 22 2022 at 09:16):From: Makarius <makarius@sketis.net>
On Tue, 14 Apr 2015, Eugene W. Stark wrote:
Since there is a thread going about various kinds of hanging, I would
like to ask about behavior that I have experienced (with Isabelle2014).
Basically the symptom is that the prover becomes unresponsive, though
JEdit does still respond. Often, the entire buffer becomes highlighted
in pink, and many times it is impossible to continue without exiting
JEdit (thereby exiting the prover) and restarting. While in the stuck
state, the prover (Poly process) exhibits constant CPU consumption. It
does not appear to be a thrashing issue because the disk traffic is low
and CPU utilization high.
This description generally sounds like a forced break due to the Poly/ML
process doing garbage collection in a tight memory situation. The
automatic heap resizing usually stays below the available physical memory,
to avoid disk thrashing for VM use, but this comes at the cost of quite
aggressive attempts to reclaim heap space. It can take 0.5 to 1 min to do
so, and the grey-pink to disappear.
However, it occurs much more often on my office machine, which is a
venerable 32-bit, one-core system with 2GB (also running Ubuntu 14.04
LTS).
That machine is indeed very old and small. I've just made some
experiments with Isabelle2015-RC1 on some virtual machine of that size.
It basically works for things like HOL/Library or HOL/Decision_Procs, but
is not much fun.
It becomes impossible if the Linux system is actually running a 64bit OS.
In that case you should make sure that the 32bit C/C++ libraries are
installed, to avoid doubling memory usage of the Poly/ML process.
These days the bottom line is at approx. 2 cores, 4 GB -- i.e. the oldest
machine that I happen to have around for testing (from 2009).
I would be interested to know what I should be looking for in order to try
to solve this. When I noticed it this morning on my home system, it appeared
to be because there were several threads occupied by various proof attempts
(I think "blast") that did not terminate. In this particular case I was
able to recover by erasing the "by blast" lines, but when things are truly
stuck (especially on the one-core system) this does not help.Another situation I have gotten into that produced similar symptoms is when
I inadvertently created recursive simplifier rules. However, I don't think
this is usually the issue.My question is: is it supposed to be possible for prover threads to hang
around indefinitely (purple mark in right margin and proof method
highlighted in purple) without timing out in some reasonable period?
If so, why, and what should I look for to try to fix the problem? If
not, then this would seem to be an issue that should be looked into.
Of course, proof tools can hang around indefinitely in their potential
non-termination. This is inherent in the game we are playing here. E.g.
an ill-behaved "by simp" or "by blast" will continue sucking up CPU
resources, until it is removed from the proof document.
The "auto" tools of the IDE are slightly different (auto quickcheck, auto
methods etc.): they have a builtin timeout. Sometimes it can still take
longer than expected to terminate non-terminating tools. I think that
"auto methods" is particularly dangerous here, but it is not enabled by
default. (It is a variant of 'try'.)
Note that Isabelle2015-RC1 has various refinements in the scheduling of
tasks. So it is worth trying to see if it makes a difference -- or if it
has newly introduced problems in the attempt to solve old problems.
Makarius
Email Gateway (Aug 22 2022 at 09:16):From: Makarius <makarius@sketis.net>
BTW, Windows 7 works quite well for such old hardware: the IDE is also a
bit more smooth, since the graphics sub-system is better supported by
Java/AWT.
Makarius
Email Gateway (Aug 22 2022 at 09:28):From: "Eugene W. Stark" <stark@cs.stonybrook.edu>
As a potentially useful point of information regarding the subject problem,
after reading some recent messages on the list that talked about the possibility
of changing the maximum number of prover threads, I went on my office machine
(the very old one-core Xeon with hyperthreading), changed the number of threads
to 2 (it was 0) and did a "isabelle build -s HOL". Now when I run Isabelle and do:
ML {* Multithreading.max_threads_value () *}
it reports 2 instead of 1. In addition, it is now possible to cancel ongoing
"try" without the looping/hanging occurring as it was before the change.
The machine is slow, obviously, but it is usable.
So I think there might be an issue (in Isabelle2014) that shows up when the
maximum number of prover threads is 1. Maybe this information will help to
identify it or at least help somebody else in the same situation.
- Gene Stark
Last updated: Apr 23 2024 at 12:29 UTC