Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] External prover crashing with SIGABRT (was: He...


view this post on Zulip Email Gateway (Apr 27 2023 at 11:21):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Here is an example of the external prover (in this case, cvc4) crash situation, which just occurred during
my current session. I include just the text output from the core dump in /var/crash, which shows the SIGABRT:

view this post on Zulip Email Gateway (Apr 27 2023 at 12:22):

From: Makarius <makarius@sketis.net>
I don't see anything specific here, probably just a spurious crash of cvc4-1.8.

This looks unrelated to questions about Isabelle/ML and Isabelle/Scala
management of tasks, threads, processes.

It does remind me that we wanted to move forward to a more recent version, but
didn't for some other reasons.

Makarius

view this post on Zulip Email Gateway (Apr 27 2023 at 12:28):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Actually, the reason we didn't move forward to cvc5 is that cvc5 crashed very often on my Intel Mac. Maybe the issue doesn't arise with other platforms and we can soon move to cvc5.

Jasmin

view this post on Zulip Email Gateway (Apr 27 2023 at 13:10):

From: Makarius <makarius@sketis.net>
Hopefully, yes.

Note that I've seen quite a lot of crashes recently on the older Intel Mac
Mini test machines that I happen to have access to.

Maybe the hardware is just degrading, or the OS versions. Or maybe some
"planned obsolescence" by Apple to get rid of the Intel platform.

Makarius

view this post on Zulip Email Gateway (Apr 27 2023 at 21:14):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I don't see this as "just a spurious crash of cvs4-1.8". I would expect a "spurious crash" to be something
like receiving SIGSEGV as a result of a null pointer exception, for example. However, in this case the signal
received is SIGABRT, as can be verified from the following line of the dump:

Signal: 6

Moreover, an unusual feature is that the process itself is in the sleep state when this occurs, as can be
verified by the following lines:

ProcStatus:
Name: cvc4
Umask: 0002
State: S (sleeping)

Now, the fact that the process is sleeping would seem to indicate that the SIGABRT was not a signal that was
generated by the process itself, but rather was sent to the process by another process. I do not think it
is possible for a process in the sleeping state to cause a signal to be sent to itself. This implies that
the abnormal termination was not the synchronous result of some erroneous action taken by the program that
caused the SIGABRT, nor even the result of an assertion in the program whose failure might have caused SIGABRT.

My recollection from my previous investigation into this issue is that SIGABRT is the signal that is sent
from the Isabelle system (Isabelle/Scala?) to cause an external prover to terminate when its results are
no longer required. Normally, the prover would have a handler installed for SIGABRT, it would catch this
signal and arrange to terminate gracefully. Indeed, that is apparently what happens most of the time.
However, sometimes it seems that SIGABRT arrives when there is not a handler installed to catch it.
In that case it causes the external prover to terminate with a core dump, which is flagged by the kernel
and which is what causes the pop-up notification and the dump file to be created in /var/crash.

In my previous investigation I do not recall being able to determine why the SIGABRT would arrive sometimes
when there was no handler for it. But, again, I do not think the behavior recorded here should be
dismissed as "just a spurious crash".

- Gene Stark

On 4/27/23 08:22, Makarius wrote:

On 27/04/2023 13:21, Eugene W. Stark wrote:

Here is an example of the external prover (in this case, cvc4) crash situation, which just occurred during
my current session.  I include just the text output from the core dump in /var/crash, which shows the SIGABRT:

ProblemType: Crash
Architecture: amd64
CrashCounter: 1
CurrentDesktop: GNOME
Date: Tue Apr 18 12:09:48 2023
DistroRelease: Ubuntu 22.04
ExecutablePath: /opt/Isabelle2022/contrib/cvc4-1.8/x86_64-linux/cvc4

I don't see anything specific here, probably just a spurious crash of cvc4-1.8.

This looks unrelated to questions about Isabelle/ML and Isabelle/Scala management of tasks, threads, processes.

It does remind me that we wanted to move forward to a more recent version, but didn't for some other reasons.

Makarius


Last updated: Mar 29 2024 at 08:18 UTC