Email Gateway (Aug 22 2022 at 12:23): Email Gateway (Aug 22 2022 at 12:23):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I apologize if I am spamming the list with problems: I am just trying to respond to
Makarius' admonition to test.
The issue I just experienced with Isabelle2016-RC2 is a lockup of JEdit in which
Java is now consuming 100% of CPU. It started with a "try" typed in the edit
window, and for awhile Java had 50% of CPU and poly had (a little less than) the other 50%,
but now it is all Java. FWIW, here is the "ps" output showing that the Java process
is actually Isabelle2016-RC2, as opposed to some random other thing running on my system:
% ps wwuax | fgrep java
gene 1009 243 11.8 6501292 2891344 pts/0 Sl 18:00 66:32
/opt/Isabelle2016-RC2/contrib/jdk/x86_64-linux/jre/bin/java -Disabelle.root=/opt/Isabelle2016-RC2 -server
-Dfile.encoding=UTF-8 -Disabelle.threads=0 -Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true
-Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Xms512m -Xmx2560m -Xss8m
-Disabelle.jedit_server=Isabelle2016-RC2 -classpath
/opt/Isabelle2016-RC2/lib/classes/Pure.jar:/opt/Isabelle2016-RC2/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar:/opt/Isabelle2016-RC2/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar:/opt/Isabelle2016-RC2/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar:/opt/Isabelle2016-RC2/contrib/jortho-1.0-2/jortho.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/akka-actor_2.11-2.3.10.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/config-1.2.1.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/jline-2.12.1.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-actors-2.11.0.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-actors-migration_2.11-1.1.0.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-compiler.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-continuations-library_2.11-1.0.2.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-continuations-plugin_2.11.7-1.0.2.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-library.jar:/opt/Isabell
e
2016-RC2/contrib/scala-2.11.7/lib/scalap-2.11.7.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-parser-combinators_2.11-1.0.4.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-reflect.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-swing_2.11-1.0.2.jar:/opt/Isabelle2016-RC2/contrib/scala-2.11.7/lib/scala-xml_2.11-1.0.4.jar:/opt/Isabelle2016-RC2/contrib/xz-java-1.2-1/lib/xz.jar:/opt/Isabelle2016-RC2/src/Tools/jEdit/dist/jedit.jar
-splash:/opt/Isabelle2016-RC2/lib/logo/isabelle.gif isabelle.Main
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 (no problem writing this mail).
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. Normally, if I get lockups, it is poly
that consumes all the CPU and JEdit stays responsive. This seems like something new.
My system:
Linux home.starkeffect.com 3.13.0-74-generic #118-Ubuntu SMP Thu Dec 17 22:52:10 UTC 2015 x86_64 x86_64 x86_64 GNU/Linux
It is an Ubuntu 14.04 LTS with pretty much up-to-date patches.
- Gene
Screenshot from 2016-01-29 18:20:34.png
Email Gateway (Aug 22 2022 at 12:23):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 12:24):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Sorry about the subject mess-up. I don't know how that happened.
I changed the subject for this follow-up -- I hope I did it in a reasonable way.
I have not changed any throttling options.
The "Enter MATCH ..." messages are produced in reasonably frequent situations when
I invoke Sledgehammer by typing "try" into the main edit window. I was aware that
they were usually throttled, but in this situation it seemed that they were not.
So maybe there is some way that the throttling gets circumvented in some situations.
- Gene Stark
Email Gateway (Aug 22 2022 at 12:24):From: Makarius <makarius@sketis.net>
That is interesting to know.
In principle, the 'try' command tries to suppress such messages, but
something might be wrong in connection to sledgehammer. Maybe Jasmin
wants to take a quick look himself.
Makarius
Last updated: Apr 19 2024 at 12:27 UTC