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



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





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