Re: [isabelle] Isabelle2016-RC2 JEdit lockup with Java at 100% CPU



On Fri, 29 Jan 2016, Eugene W. Stark wrote:

The issue I just experienced with Isabelle2016-RC2 is a lockup of JEdit in which
Java is now consuming 100% of CPU.

-Xms512m -Xmx2560m -Xss8m

I've attached a screenshot showing results from "top". As you can see it has been some time and it has not recovered. The JEdit window is unresponsive, but the rest of the system is OK.

Top shows resident memory for "java" above 2.7g, so the JVM is in normal crisis situation of full heap space (specified as -Xmx2560m above).

Depending how much total memory you have, you can make this a bit more generous, e.g. in the file Isabelle2016-RC2.options64 (if you use the toplevel application).

I have 32GB and usually give -Xmx4096m to java, which is sufficient for all practical situations in Isabelle + AFP.


I tried using Eclipse/JVM Monitor to connect to the JVM and see what is going on in there, but it reports that Hotspot is not enabled for that process. So not much other information I can provide, other than that it has occurred.

I don't know anything about Eclipse, and normally use the simple "jconsole" tool that is included in the JDK distribution. It sometimes helps to push the "GC" button there, but probably not in this situation.


Normally, if I get lockups, it is poly that consumes all the CPU and JEdit stays responsive.

You should make double sure that Poly/ML runs in x86 (32bit) mode, to reduce memory requirements by a factor of 2. (I think you have that, guessing from the "top" output, but just make sure anyway.) You can see that in the output of "isabelle build -?" for example.


The general question remains, if your application is really that large, or if there are other problems (e.g. memory holes).

Otherwise I would say it is a matter of normal Harley-Davidson tuning to make the best of limited resources.


	Makarius





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