Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] run-away Isabelle process

Email Gateway (Aug 22 2022 at 09:46):

From: "Elsa L. Gunter" <egunter@illinois.edu>
Dear Isabelle Community,
I am having grave problems with the execution of Isabelle-2014, and I
have not found a thread on this mailing list that seems to address my
problem. Isabelle is taking arbitrarily long in between steps of proof,
and other things, where arbitrarily long is minutes to hours to
overnight without completing. And while I suspect that I may be
contributing to the problem by there being a rewrite that I have added
that has led to a non-confluent system, the system tight now has taken
more then an hour to try to do a thin_tac, which should never be
non-terminating. And despite the length of time I have waited, it
almost surely will come back, eventually (in the temporal logic sense of
unbounded eventually). But this is making it really painful to try to
make any progress.
Some background for anybody who might have an idea how to help me.
First, my system is a mac running Mac OX X 10.9.5 (maverick, with
patches); processor is a 2.8 GHz Intel Core 17 with 4 cores (1
processor), 16 GB 1600 MHz DDR3 Memory. I am running Isabelle 2014 with
a fairly recent version of the Archive of Formal Proofs. My preferences
file is quite minimal, and makes no mention of threads. My code
depends on the List-Infinite and JinjaThreads. I have a collection of
twelve locally developed theories upon which I also depend. The local
theories accumulate to something more than 10000 loc. I have previously
built a heap containing the AFP theories, and I start form that heap. I
thought I might reduce the problem by building a heap containing the all
the local theories upon which I depend, but that build never terminated
(I let it run overnight, ~10 hours). I found that strange, since it
takes about 10 minutes for it to build the local theories upon which I
am depending when I am interactively loading the desired theory from a
base containing just the AFP stuff I need. I've tried it twice, but it
is a time-consuming, unproductive exercise.
When Isabelle is semi-non-responsive, it usually colors all of the
text grey (not purple). I haven't been able to tell which of the greys
it is. Just now, while writing this message, the thin_tac I requested
can back (correctly), and then I deleted the line after it, causing the
cursor to be again immediately after the thin_tac. The text was greyed
out again, and then after a couple of minutes it became clear with the
thin_tac line yellow, but it is failing to display the output. I
presume it will in a little while. I have had problems along these
lines, but less severe ever since switching to jEdit from Proof General,
with the problem seeming to grow some since the beginning of the
semester (January), but with it getting an order of magnitude worse in
the last week. The problem's getting worse seemed to be temporally
correlated with my doing a proof that involved a term that was about 40
lines long (the term, that is). Other than that, I'm not using metis or
smt, and rarely auto or force or blast. simp and clarsimp get used a
fair amount, so nonterminating rewrites might have something to do with
my problem, except I would expect it to just always fail to come back,
which is not its behavior. There are a few bits of orange (warnings) in
some of the files upon which I depend, but I have removed them all from
the current file. I have observed that ambiguous parses, where only one
is type correct, slow Isabelle down very considerably. My proofs ar a
mix of Isar style and old apply style, with most of the recent additions
being in the old apply style. I do have a fairly large number of
locales I'm working with, and doing a print_locale! is just out of the
question. Each time the evaluation has to go through the creation of a
new layer of locale by combining specialized versions of previous one,
together with additions, that is always a choke point in the
computation. I can't think of any other observations I have made that
might be relevant.
This matter is rather urgent to me. I am teaching a course this
semester based on the use of Isabelle, with students working on a large
combined project, each with his or her own part. I need to be helping
them fairly regularly, in part by giving them extra lemmas about the
core infrastructure that groups of them need to overcome various hurdles
they face in their subprojects. I have told them lemma statements to
add to their code with a sorry, and they are proceeding with these, but
the course ends next week, and it would be a great pity not to be able
to provide them with a sense of closure from having all theorems really
and truly proved. Also, so far the students do not seem to be
struggling with Isabelle delays to the extent I am, but if they suddenly
start having the same problems, I can not feasibly ask them to continue
their work, with would definitely leave them with a lack of closure. I
would appreciate any help anyone can give to improve this situation.
---Elsa

Email Gateway (Aug 22 2022 at 09:47):

From: Makarius <makarius@sketis.net>
On Sun, 3 May 2015, Elsa L. Gunter wrote:

I am having grave problems with the execution of Isabelle-2014, and I
have not found a thread on this mailing list that seems to address my
problem.

It generally sounds like a situation close to the proverbial "concrete
wall" of system resource limits. Only black holes and national debts can
grow indefinitely, and for black holes it is not yet sure.

Below are some hints how to stretch resource paramaters a bit, and thus
postpone the imminent meltdown.

Isabelle is taking arbitrarily long in between steps of proof, and other
things, where arbitrarily long is minutes to hours to overnight without
completing.

In such situations it is important to get an idea which part of Isabelle
is busy. There are two sides: Isabelle/ML and Isabelle/Scala,
corresponding to two run-time system processes: poly and java. With "top
-o cpu" on the command-line of Mac OS X it should be possible to see a bit
more.

Moreover, a Java process can be analyzed by jconsole, to get an idea about
heap size, threads etc. This tool is part of the bundled JDK of Isabelle
in $JAVA_HOME/bin -- you can find that out as follows inside Isabelle:

ML {* getenv "JAVA_HOME" *}

And while I suspect that I may be contributing to the problem by there
being a rewrite that I have added that has led to a non-confluent
system, the system tight now has taken more then an hour to try to do a
thin_tac, which should never be non-terminating.

Non-termination alone should not be a problem: you get deep-purple
feedback in the Prover IDE, and should be able to delete the material to
recover. Serious problems are usually caused by:

(a) Massive amounts of "potentially useful tracing information" that
tool implementors sometimes leave in by default (which is very bad
programming style). That is the easyiest way to bomb the front-end.

(b) Really huge intermediate goal states that are printed, either
accidentally or on purpose, e.g. via print_tac. It occasionally
helps to reduce output size like this:

declare [[goals_limit = 1, show_markup = false]]

My code depends on the List-Infinite and JinjaThreads. I have a
collection of twelve locally developed theories upon which I also
depend. The local theories accumulate to something more than 10000 loc.

This is already quite substantial material. JinjaThreads is always at
120% of system resources, no matter how much are available.

I have previously built a heap containing the AFP theories, and I start
form that heap. I thought I might reduce the problem by building a heap
containing the all the local theories upon which I depend, but that
build never terminated (I let it run overnight, ~10 hours). I found
that strange, since it takes about 10 minutes for it to build the local
theories upon which I am depending when I am interactively loading the
desired theory from a base containing just the AFP stuff I need.

Here I suspect that the JVM default heap is too small for this amount of
sources. Try something like this in $ISABELLE_HOME_USER/etc/settings:

ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms1024m -Xmx4096m -Xss4m"

Using a suitable base image can significantly reduce the resource
requirements of the Prover IDE. Note that the build of the selected base
session of the Prover IDE actually uses the JVM parameters of
Isabelle/jEdit. The above only applies to "isabelle build" on the
command-line.

When Isabelle is semi-non-responsive, it usually colors all of the text
grey (not purple). I haven't been able to tell which of the greys it
is.

That could be outdated_color. You can change the color value in Plugin
Options / Isabelle / Rendering to check this hypothesis.

Just now, while writing this message, the thin_tac I requested can back
(correctly), and then I deleted the line after it, causing the cursor to
be again immediately after the thin_tac. The text was greyed out again,
and then after a couple of minutes it became clear with the thin_tac
line yellow, but it is failing to display the output. I presume it will
in a little while.

Here it is again important to know if poly or java is busy, or both. For
example, it could be a rather long garbage collection of Poly/ML, which is
normal with JinjaThreads in the back. To amend this, you should use
Poly/ML in 64bit mode like this in $ISABELLE_HOME_USER/etc/settings:

ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$ML_HOME/../$ML_PLATFORM"

Another possibility is JVM heap space. You can enlarge that for the
Prover IDE in the .app bundle Info.plist in its <key>JVMOptions</key>
entry. For the command-line version of "isabelle jedit" the same
information is in $ISABELLE_HOME_USER/etc/settings e.g.:

JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"

In both situations, you need to "reboot" the application.

The problem's getting worse seemed to be temporally correlated with my
doing a proof that involved a term that was about 40 lines long (the
term, that is).

I have observed that ambiguous parses, where only one is type correct,
slow Isabelle down very considerably.

Ambiguous grammars or input can cause exponential blowup of parse trees.
With rather large terms, this can be a real problem.

I do have a fairly large number of locales I'm working with, and doing a
print_locale! is just out of the question. Each time the evaluation has
to go through the creation of a new layer of locale by combining
specialized versions of previous one, together with additions, that is
always a choke point in the computation.

JinjaThreads is already stretching locales and locale interpretation
beyond feasibilty. If you build on top of some very big locales of that
session, it is likely to cause problems.

Makarius

Email Gateway (Aug 22 2022 at 09:49):

From: "Elsa L. Gunter" <egunter@illinois.edu>
On 5/3/15 2:22 PM, Makarius wrote:

On Sun, 3 May 2015, Elsa L. Gunter wrote:

I am having grave problems with the execution of Isabelle-2014, and I
have not found a thread on this mailing list that seems to address my
problem.

It generally sounds like a situation close to the proverbial "concrete
wall" of system resource limits. Only black holes and national debts
can grow indefinitely, and for black holes it is not yet sure.

Below are some hints how to stretch resource paramaters a bit, and
thus postpone the imminent meltdown.

Isabelle is taking arbitrarily long in between steps of proof, and
other things, where arbitrarily long is minutes to hours to overnight
without completing.

In such situations it is important to get an idea which part of
Isabelle is busy. There are two sides: Isabelle/ML and
Isabelle/Scala, corresponding to two run-time system processes: poly
and java. With "top -o cpu" on the command-line of Mac OS X it should
be possible to see a bit more.
Using the Activity monitor, it is primarily poly that is primary
resource hog. It is running at ~ 400% - 450~ cpu. If I run top -o cpu
for a second or two and redirect the output to a file, poly will always
exactly occur once near the top:

659 poly403.8 81:49:39 14/4 0 28 12133 12G+ 12G- 0B

and JavaAppLaunc occurs repeatedly, lower down:

623 JavaAppLaunc 0.1 19:47.99 65 7 333 2179 280M+
307M+ 0B

Moreover, a Java process can be analyzed by jconsole, to get an idea
about heap size, threads etc. This tool is part of the bundled JDK of
Isabelle in $JAVA_HOME/bin -- you can find that out as follows inside
Isabelle:

ML {* getenv "JAVA_HOME" *}

I can't do that right now (unless I kill my Isabelle process and
restart) because Isabelle isn't paying any attention to me right now,
for the last half hour.

And while I suspect that I may be contributing to the problem by
there being a rewrite that I have added that has led to a
non-confluent system, the system tight now has taken more then an
hour to try to do a thin_tac, which should never be non-terminating.

Non-termination alone should not be a problem: you get deep-purple
feedback in the Prover IDE, and should be able to delete the material
to recover. Serious problems are usually caused by:

(a) Massive amounts of "potentially useful tracing information" that
tool implementors sometimes leave in by default (which is very bad
programming style). That is the easyiest way to bomb the
front-end.
show_types is off, and I'm not tracing anything (although I would like
to if I dared).

(b) Really huge intermediate goal states that are printed, either
accidentally or on purpose, e.g. via print_tac. It occasionally
helps to reduce output size like this:

declare [[goals_limit = 1, show_markup = false]]
I can do that, although mostly the size of each step is not that big.
The thing it is currently stuck on is only one goal that is 20 lines
long with 6 short assumptions that are only one line a piece.

My code depends on the List-Infinite and JinjaThreads. I have a
collection of twelve locally developed theories upon which I also
depend. The local theories accumulate to something more than 10000 loc.

This is already quite substantial material. JinjaThreads is always at
120% of system resources, no matter how much are available.

I'm not actually taking all of JinjaThreads, but cherry picking the
concurrency parts, since I'm not actually doing anything with Jinja/Java
in this project (although I am in another).

I have previously built a heap containing the AFP theories, and I
start form that heap. I thought I might reduce the problem by
building a heap containing the all the local theories upon which I
depend, but that build never terminated (I let it run overnight, ~10
hours). I found that strange, since it takes about 10 minutes for it
to build the local theories upon which I am depending when I am
interactively loading the desired theory from a base containing just
the AFP stuff I need.

Here I suspect that the JVM default heap is too small for this amount
of sources. Try something like this in $ISABELLE_HOME_USER/etc/settings:

ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms1024m
-Xmx4096m -Xss4m"
I will try adding this to my settings.

Using a suitable base image can significantly reduce the resource
requirements of the Prover IDE. Note that the build of the selected
base session of the Prover IDE actually uses the JVM parameters of
Isabelle/jEdit. The above only applies to "isabelle build" on the
command-line.

I've been building my heaps via isabelle jEdit -d <<path to ROOT,
typically .>> -l <<heap name>> instead of using isabelle build, because
I was having trouble with isabelle build and I thought you said you
always went through a command-line call to isabelle jEdit.

When Isabelle is semi-non-responsive, it usually colors all of the
text grey (not purple). I haven't been able to tell which of the
greys it is.

That could be outdated_color. You can change the color value in
Plugin Options / Isabelle / Rendering to check this hypothesis.

Which field should I change? There are several greys, and my eyes
aren't good enough to tell them apart.

Just now, while writing this message, the thin_tac I requested can
back (correctly), and then I deleted the line after it, causing the
cursor to be again immediately after the thin_tac. The text was
greyed out again, and then after a couple of minutes it became clear
with the thin_tac line yellow, but it is failing to display the
output. I presume it will in a little while.

Here it is again important to know if poly or java is busy, or both.
For example, it could be a rather long garbage collection of Poly/ML,
which is normal with JinjaThreads in the back. To amend this, you
should use Poly/ML in 64bit mode like this in
$ISABELLE_HOME_USER/etc/settings:

ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$ML_HOME/../$ML_PLATFORM"
I am using Isabelle is 64 bit mode, as per an earlier suggestion you
made to me. My setting file contains extactly:

ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--minheap 2000 --maxheap 12000"

Another possibility is JVM heap space. You can enlarge that for the
Prover IDE in the .app bundle Info.plist in its <key>JVMOptions</key>
entry. For the command-line version of "isabelle jedit" the same
information is in $ISABELLE_HOME_USER/etc/settings e.g.:

JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
I will add this too, and try rebooting the application. And I will run
it from the command-line, at least unitl that proves not to work as well.

In both situations, you need to "reboot" the application.

The problem's getting worse seemed to be temporally correlated with
my doing a proof that involved a term that was about 40 lines long
(the term, that is).

I have observed that ambiguous parses, where only one is type
correct, slow Isabelle down very considerably.

Ambiguous grammars or input can cause exponential blowup of parse
trees. With rather large terms, this can be a real problem.

The term was not ambiguous, and because I have observed the grief
ambiguous terms cause, I have removed most mixfix syntax from my input
code. I would be useful if I could shut off the pretty printing for
mixfix as well so that isabelle could parse what it prints. I have shut
off abbreviations, but i have not found a flag for the mixfix.

I do have a fairly large number of locales I'm working with, and
doing a print_locale! is just out of the question. Each time the
evaluation has to go through the creation of a new layer of locale by
combining specialized versions of previous one, together with
additions, that is always a choke point in the computation.

JinjaThreads is already stretching locales and locale interpretation
beyond feasibilty. If you build on top of some very big locales of
that session, it is likely to cause problems.

We are only borrowing the theory of bisimulation from JinjaThreads, not
the whole Jinja concurrent semantics. bisimulation alone is big, but I
thought it was less than a quarter of all of JinjaThreads. I could be
wrong, but I think the total code I'm adding on top of bisimulation is
less than the amount I have left out of JinjaThreads.

Makarius
Thank you for your attempt to help me. If the changes to the settings
helps, I will let you know.
---Elsa

Email Gateway (Aug 22 2022 at 09:52):

From: Makarius <makarius@sketis.net>
On Sun, 3 May 2015, Elsa L. Gunter wrote:

Using the Activity monitor, it is primarily poly that is primary resource
hog. It is running at ~ 400% - 450~ cpu. If I run top -o cpu for a second
or two and redirect the output to a file, poly will always exactly occur once
near the top:

659 poly403.8 81:49:39 14/4 0 28 12133 12G+ 12G- 0B

Here we see 12G already, which means Poly/ML is practically at the maximum
of your 16GB machine.

and JavaAppLaunc occurs repeatedly, lower down:

623 JavaAppLaunc 0.1 19:47.99 65 7 333 2179 280M+ 307M+
0B

I can't say on the spot if this is the actual JVM run-time system. It
might be just the launcher, and a second big "java" process is elsewhere.
Normally the Prover IDE requires a few GB for such big things.

I'm not actually taking all of JinjaThreads, but cherry picking the
concurrency parts, since I'm not actually doing anything with Jinja/Java in
this project (although I am in another).

OK. Do you have all that base material in the base heap image? Or is it
loaded into the Prover IDE interactively?

When Isabelle is semi-non-responsive, it usually colors all of the text
grey (not purple). I haven't been able to tell which of the greys it
is.

That could be outdated_color. You can change the color value in Plugin
Options / Isabelle / Rendering to check this hypothesis.

Which field should I change? There are several greys, and my eyes aren't
good enough to tell them apart.

The left column has all colors in alphabetical order. There should be an
entry "Outdated color" with some pinkish grey.

I would be useful if I could shut off the pretty printing for mixfix as
well so that isabelle could parse what it prints. I have shut off
abbreviations, but i have not found a flag for the mixfix.

If it is your own mixfix syntax, you could specify an explicit print mode
and turn that on/off on demand. But I don't think that is needed: doing
mixfix syntax right, without ambiguities, it should parse and print
nicely.

We are only borrowing the theory of bisimulation from JinjaThreads, not
the whole Jinja concurrent semantics. bisimulation alone is big, but I
thought it was less than a quarter of all of JinjaThreads. I could be
wrong, but I think the total code I'm adding on top of bisimulation is
less than the amount I have left out of JinjaThreads.

This sounds quite reasonable. JinjaThreads contains many interesting
things, well-hidden to potentially interested parties.

If you want, you can send me your development privately, so that I can
experiment with it a bit on my modest 12 core, 32 GB machine.

Makarius

Email Gateway (Aug 22 2022 at 10:00):

From: "Elsa L. Gunter" <egunter@illinois.edu>
Dear Makarius,
Your previous message got me enough wiggle room to get the immediate
theorm I was working on to go through.

On 5/3/15 3:48 PM, Makarius wrote:

On Sun, 3 May 2015, Elsa L. Gunter wrote:

Using the Activity monitor, it is primarily poly that is primary
resource hog. It is running at ~ 400% - 450~ cpu. If I run top -o
cpu for a second or two and redirect the output to a file, poly will
always exactly occur once near the top:

659 poly403.8 81:49:39 14/4 0 28 12133 12G+
12G- 0B

Here we see 12G already, which means Poly/ML is practically at the
maximum of your 16GB machine.

and JavaAppLaunc occurs repeatedly, lower down:

623 JavaAppLaunc 0.1 19:47.99 65 7 333 2179 280M+
307M+ 0B

I can't say on the spot if this is the actual JVM run-time system. It
might be just the launcher, and a second big "java" process is
elsewhere. Normally the Prover IDE requires a few GB for such big things.
I don't see java itself showing up. I think polyml is the hog.

I'm not actually taking all of JinjaThreads, but cherry picking the
concurrency parts, since I'm not actually doing anything with
Jinja/Java in this project (although I am in another).

OK. Do you have all that base material in the base heap image? Or is
it loaded into the Prover IDE interactively?
Almost. There is a in List-Inifinite that needs to be included because
of some reorganizing of the AFP entry. Everything I need from
JinjaThreads is in my precompiled heap.

When Isabelle is semi-non-responsive, it usually colors all of
the text > grey (not purple). I haven't been able to tell which of
the greys it > is.

That could be outdated_color. You can change the color value in
Plugin
Options / Isabelle / Rendering to check this hypothesis.

Which field should I change? There are several greys, and my eyes
aren't good enough to tell them apart.

The left column has all colors in alphabetical order. There should be
an entry "Outdated color" with some pinkish grey.

OK. I have changed it to a kind of light lime green that I think I will
not confuse with anything else. Since it isn't choking yet (although it
still runs at 200% CPU with over 8 GB of memory when I have not
requested it to do anything), I cn't tell it tha tis the color of a choke.

Just what is Isabelle (polyml) doing when the cursor is sitting at the
end of a fully successfully completed proof? I would have expected it
to be waiting for user input before doing anything else, but it keeps
running something. The energy impact of Isabelle is over ten times more
than everything else on my system combined, and I'm lazy about leaving
stuff around.

It would be useful if I could shut off the pretty printing for mixfix
as well so that isabelle could parse what it prints. I have shut off
abbreviations, but i have not found a flag for the mixfix.

If it is your own mixfix syntax, you could specify an explicit print
mode and turn that on/off on demand. But I don't think that is
needed: doing mixfix syntax right, without ambiguities, it should
parse and print nicely.
I have not found all the sources of the ambiguities, but loading two
different theories that sue syntax that is unambiguous in itself can
lead to ambiguous syntax. Since there are no checks the mixfix syntax
has been done right, it would be nice to have a way of pretty printing
that was guaranteed to parse. Shutting off mixfix I believe would do that.

We are only borrowing the theory of bisimulation from JinjaThreads,
not the whole Jinja concurrent semantics. bisimulation alone is big,
but I thought it was less than a quarter of all of JinjaThreads. I
could be wrong, but I think the total code I'm adding on top of
bisimulation is less than the amount I have left out of JinjaThreads.

This sounds quite reasonable. JinjaThreads contains many interesting
things, well-hidden to potentially interested parties.

If you want, you can send me your development privately, so that I can
experiment with it a bit on my modest 12 core, 32 GB machine.

Makarius

Thank you for your help and your offer for more. I hope/think I can now
limp through the next week. However, this has caused me to wonder how I
can continue to use Isabelle for the project on which I am embarked. I
am only at the beginning and if I am running out of resources now, I'm
not sure how I could hope to carry my project to completion.
---Elsa

Email Gateway (Aug 22 2022 at 10:02):

From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hello Elsa.

I'm not completely sure about this, but I have taken the following
actions a couple of times and I think they might have reduced polyML's
memory footprint.

1) Restart Isabelle if polyML is getting too big. I am anecdotally
convinced that sometimes polyML's heap size drifts upwards over time,
and that a restart can reset this.

2) Try enabling "skip-proofs" during the reset while rebuilding up to
where you were before. You can find an option for skipping proofs in
Isabelle's options panel: jEdit menu Plugins->Plugin Options, pick
Isabelle->General, find the skip proofs setting. This will not only save
time, it will cause polyML to build less proof-related objects
internally, which may save memory.

Caveat emptor ; all of the above may simply be a superstitious ritual I
go through as a result of confirmation bias.

Good luck,
Thomas.

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Email Gateway (Aug 22 2022 at 10:03):

From: "Elsa L. Gunter" <egunter@illinois.edu>
Thank you, Thomas. I will add these to my set of options.
---Elsa

Email Gateway (Aug 22 2022 at 10:03):

From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Another strategy I find useful is processing the following line when you're running very low on
available memory, which I believe forces a garbage collection.

ML {* PolyML.fullGC () *}

Forcing a garbage collection in a managed language seems rather silly, but I have found it is
sometimes the only way to regain a responsive system.

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Email Gateway (Aug 22 2022 at 10:04):

From: Makarius <makarius@sketis.net>
On Sun, 3 May 2015, Elsa L. Gunter wrote:

Since it isn't choking yet (although it still runs at 200% CPU with over
8 GB of memory when I have not requested it to do anything), I cn't tell
it tha tis the color of a choke.

Just what is Isabelle (polyml) doing when the cursor is sitting at the
end of a fully successfully completed proof? I would have expected it
to be waiting for user input before doing anything else, but it keeps
running something. The energy impact of Isabelle is over ten times more
than everything else on my system combined, and I'm lazy about leaving
stuff around.

Isabelle/PIDE is no longer based on a TTY loop, so it is not really
waiting for the next user input. Rather the editor is continously
streaming edits towards the prover, and the prover continously streaming
results towards the editor. In practice, this eventually converges, and
both sides can become mostly idle, except for a few percent of CPU time.

If you see 200% CPU usage of poly, despite nothing really going on, it is
something to be investigated. E.g. there could be a bit too much garbage
collection due to excessive use of heap space. Or there could be "auto
tools" that did not terminate and could not be canceled properly, or even
just long-running tasks to print proof states after scrolling in the
editor.

Isabelle/jEdit also has a Monitor panel to inspect certain aspects of the
ML run-time system.

I hope/think I can now limp through the next week. However, this has
caused me to wonder how I can continue to use Isabelle for the project
on which I am embarked. I am only at the beginning and if I am running
out of resources now, I'm not sure how I could hope to carry my project
to completion.

Looking in just the right corners of big projects usually helps to get a
factor 2 improvement concerning resource usage.

Moreover, I have already some ideas to reduce the ML heap space
requirements once again, but not for this release of Isabelle2015. The
question is how long we can hold out in 32bit address space, without
having to move to 64bit and thus practically into the cloud, e.g. see the
sketches on my blog
http://sketis.net/2015/proposal-remote-prover-connectivity-for-isabellepide

Makarius

Email Gateway (Aug 22 2022 at 10:07):

From: Makarius <makarius@sketis.net>
Here is a rather drastic way to reclaim a lot of heap space by maximal
sharing of equal data structures:

ML "ML_System.share_common_data ()"

It can take minutes, but can shrink the heap by a factor of 2-3, or more.
This is normally used when dumping heap images.

A limited form of that is also used in normal operation of the Poly/ML
runtime-system. It is the reason why most applications still work within
the tiny 32bit address space.

David Matthews can say more about the various GC phases of Poly/ML.

The "Monitor" dockable in Isabelle/jEdit also has a heap section, which
helps to get some idea about resource usage, and the effect of the above
operations. Note that while the run-time system is busy doing such jobs,
there is no update of the statistics, because the ML user space is
inactive.

Makarius

Email Gateway (Aug 22 2022 at 10:08):

From: David Matthews <dm@prolingua.co.uk>
The garbage collector isn't just a simple case of: run out of heap;
perform GC; resume. Or at least it hasn't been for a very long time.
The GC code has to decide whether to run a cheap, but incomplete minor
collection; a full but more expensive major collection; increase or
sometimes decrease the size of the heap or run the very expensive data
sharing pass that Makarius mentions. There's no easy answer to this
because it depends on the pattern of allocations and the kind of data
structures being built. Indeed the best choice would really depend on
what happens AFTER the collection; the application may be just on the
point of completing when the GC decides to start an expensive operation.

The GC has heuristics to help decide what to do and uses the results of
previous choices to guide the next choice. For example, if a sharing
pass was run and found lots of sharing it may be worth running it sooner
rather than later. Much of the tuning was done by looking at large
Isabelle problems and JinjaThreads was the archetypal example.

I'm very happy to look at this and see whether the tuning can be
improved or indeed if garbage collection is the issue or not. It may be
that there needs to be some extra hints to the GC that can be given as
command line arguments in situations where a user is approaching the
limits on their machine. One suggestion I'd make is to increase the
value of --maxheap closer to the memory available on your machine (e.g.
--maxheap 14000). It's not a good idea to increase it above the
physical memory size since that can introduce thrashing but if you're
close to the limit it could be better to tolerate a bit of it.

David

Last updated: Nov 21 2024 at 12:39 UTC