overlapping calls to proof-shell-filter

[Hendrik Tews]

Hi,

sometimes I see prooftree crashes with a cold disk cache (eg
after reboot or after "sync; sudo sh -c 'echo 3 >
/proc/sys/vm/drop_caches'").

What apparently happens is that at some stage process-send-string
blocks because the pipe to prooftree is full. This happens inside
proof-shell-filter, because the prooftree display commands are
created and sent when output arrives from Coq.

When I/O blocks, Emacs automatically accepts output processes. So
it calls proof-shell-filter again before the previous call
finished. Finally some garbage or truncated messages is written
to the pipe and prooftree crashes.

It should definitely not happen that proof-shell-filter is called
while another instance is still running. Does anybody know a way
to ensure this?

Bye,

Hendrik

[David Aspinall]

Hello Hendrik

Quick thoughts: this sounds like a pretty fundamental problem and
surprising if we hadn't come across it before. Do you definitely see
this in the ordinary running code, not just when using the debugger?
Maybe prooftree input is different case to prover input.

If we need to fix it, I suppose we could try to exit the PG filter
function early using our own flag to detect nested calls. A more robust
mechanism might be to try to send new input from the main event loop
instead, but that would be a significant reworking. (Or could you do
that just for proof tree?)

- David

Post by Hendrik Tews
Hi,
sometimes I see prooftree crashes with a cold disk cache (eg
after reboot or after "sync; sudo sh -c 'echo 3 >
/proc/sys/vm/drop_caches'").
What apparently happens is that at some stage process-send-string
blocks because the pipe to prooftree is full. This happens inside
proof-shell-filter, because the prooftree display commands are
created and sent when output arrives from Coq.
When I/O blocks, Emacs automatically accepts output processes. So
it calls proof-shell-filter again before the previous call
finished. Finally some garbage or truncated messages is written
to the pipe and prooftree crashes.
It should definitely not happen that proof-shell-filter is called
while another instance is still running. Does anybody know a way
to ensure this?
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

[Hendrik Tews]

David Aspinall <David.Aspinall-***@public.gmane.org> writes:

Quick thoughts: this sounds like a pretty fundamental problem and
surprising if we hadn't come across it before. Do you definitely see
this in the ordinary running code, not just when using the debugger?

I don't use the debugger, I let certain functions insert start
and end messages into a dedicated buffer. There, I see
proof-shell-filter starting before the previous instance
finished.

In principle, the problem can also appear without prooftree.
Proof General will block when sending a sufficiently large
command. If the proof assistant generates output before
completely reading the command, proof-shell-filter might get
called a second time. The command has to be really large, because
default pipe size is 64K since Linux 2.6.11.

If we need to fix it, I suppose we could try to exit the PG filter
function early using our own flag to detect nested calls.

Yes, using a second flag to remember aborted nested calls, such
that proof-shell-filter can call itself recursively if a nested
call was aborted.

Am I right, that proof-shell-filter does not use its ``str''
argument?

Because the problem does only appear when starting prooftree with
cold disk caches (which takes more than 1 sec on my laptops), a
partial fix would be to block Proof General until prooftree is
ready.

(Or could you do that just for proof tree?)

I don't understand. The problem appears, because it takes more
than one second until prooftree is ready and Coq + Proof General
generate more than 64K display commands in that time.

Bye,

Hendrik

[Hendrik Tews]

Hi,

here is a patch that solves the problem for me. Any comments?

Bye,

Hendrik

[Stefan Monnier]

+In Emacs a process filter function can be called while the same
+filter is currently running for the same process, for instance,
+when the filter bocks on I/O. This wrapper protects the main

I think this deserves an Emacs bug report. I'm not completely sure it's
a bug rather than a "feature", but it would be good to record this as
a problematic area. I think many packages are vulnerable to this
problem, although they usually don't suffer from it. The most common
case where they do suffer from it is when you try to Edebug the
process filter.


Stefan

[Hendrik Tews]

Stefan Monnier <monnier-***@public.gmane.org> writes:

I think this deserves an Emacs bug report.

see http://debbugs.gnu.org/cgi/bugreport.cgi?bug=13400

There are definitely some documentation problems.
process-send-string is not mentioned as function that might
trigger a filter call.

I think many packages are vulnerable to this
problem, although they usually don't suffer from it. The most common
case where they do suffer from it is when you try to Edebug the
process filter.

I believe it would be good to have a process-specific flag that
inhibits overlapping parallel calls to the same process filter.
Emacs could accept output but buffer it until the previous filter
terminates.

Bye,

Hendrik

[Stefan Monnier]

Post by Stefan Monnier
I think this deserves an Emacs bug report.
see http://debbugs.gnu.org/cgi/bugreport.cgi?bug=13400

Thanks,


Stefan

[David Aspinall]

At a quick glance this looks like a reasonable way to fix without
messing with the current filter code. Luckily, I don't think the str
argument is used. I'm not completely clear on the error case, is the
idea just to give up if we hit an error in some call?

- D.

Post by Hendrik Tews
Hi,
here is a patch that solves the problem for me. Any comments?
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

[Hendrik Tews]

David Aspinall <David.Aspinall-***@public.gmane.org> writes:

At a quick glance this looks like a reasonable way to fix without
messing with the current filter code. Luckily, I don't think the str
argument is used.

I'm not completely clear on the error case, is the
idea just to give up if we hit an error in some call?

If proof-shell-filter signals an error, the error is just
propagated, only the active flag is reset to enable later calls
again.

Or do you mean the case where a parallel, overlapping call is
detected? In this case the -was-blocked flag is set and the
already running instance of the wrapper stays for one more
iteration in the while loop, thus calling proof-shell-filter
after the previous call finished.

This effectively delays Coq until prooftree catches up. This is
just what you want, I believe.

Under normal circumstances prooftree is much faster than Coq.
Because of the experience with PVS, where the proof tree
visualizer was often the bottleneck, I made some special
optimizations:

- tree layout is linear in the tree depth; for PVS it is
apparently worse than linear in the number of nodes

- tree display is delayed until no display commands are available
on input; nevertheless, when asserting large regions, you see
the tree growing node by node, indicating that prooftree is
faster than Coq

Bye,

Hendrik

[Hendrik Tews]

I wrote:

here is a patch that solves the problem for me. Any comments?

I committed now. I deleted the argument of proof-shell-filter, to
make sure, nobody will use it. Reasons are described in the doc
comments.

Hendrik