Re: [isabelle] "Stuck" (i.e. looping) prover issues

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

On 04/17/2015 06:39 PM, Makarius wrote:
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.


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