Email Gateway (Aug 22 2022 at 14:24): Email Gateway (Aug 22 2022 at 14:24):From: Makarius <makarius@sketis.net>
I am only partly involved here, as provider of Isabelle_System.bash,
which is the place where SIGINT, SIGTERM, SIGKILL are sent to external
processes (the latter signals only occur when processes resist
termination on plain SIGINT 10 times).
The reason for such signals are usually Timeout.timeout in ML, or just
the user editing PIDE document content, such that old attempts of
evaluation are discontinued -- user edits can be quite erratic.
Looking through the cvc4 sources, I've found several signal handlers
here: https://github.com/CVC4/CVC4/blob/master/src/main/util.cpp --
they usually end with abort(), which causes SIGABRT on the process.
I am not proficient in C++ system programming and can't say if there is
something wrong on the cvc4 side. At a high-level, a process that reacts
strangely when sent SIGINT looks bad, but in some sense it is also a
very common situation -- reminds me of E prover some years ago.
Isabelle as interactive system works under the global assumption that
all internal and external processes can always be interrupted cleanly.
Shall we hand this over to the cvc4 guys? There might be still enough
time for our release, to get a clarification of this important fine point.
Makarius
Email Gateway (Aug 22 2022 at 14:28):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Unfortunately, the --no-statistics option does not work to suppress the aborts.
With Isabelle-2016-1-RC3:
ERROR: apport (pid 3688) Sat Nov 26 08:39:13 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3700) Sat Nov 26 08:39:20 2016: called for pid 3695, signal 6, core limit 0
ERROR: apport (pid 3700) Sat Nov 26 08:39:20 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 6418
/tmp/isabelle-gene/process7458968389934499957/cache-io-3949674")
ERROR: apport (pid 3700) Sat Nov 26 08:39:20 2016: debug: session gdbus call: (true,)
ERROR: apport (pid 3700) Sat Nov 26 08:39:20 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3712) Sat Nov 26 08:39:24 2016: called for pid 3711, signal 6, core limit 0
ERROR: apport (pid 3712) Sat Nov 26 08:39:24 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 4058
/tmp/isabelle-gene/process7458968389934499957/cache-io-3952234")
ERROR: apport (pid 3712) Sat Nov 26 08:39:24 2016: debug: session gdbus call: (true,)
ERROR: apport (pid 3712) Sat Nov 26 08:39:24 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3728) Sat Nov 26 08:39:28 2016: called for pid 3720, signal 6, core limit 0
ERROR: apport (pid 3728) Sat Nov 26 08:39:28 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 3000
/tmp/isabelle-gene/process7458968389934499957/cache-io-3953574")
ERROR: apport (pid 3728) Sat Nov 26 08:39:28 2016: debug: session gdbus call: (true,)
ERROR: apport (pid 3728) Sat Nov 26 08:39:28 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3743) Sat Nov 26 08:39:31 2016: called for pid 3737, signal 6, core limit 0
ERROR: apport (pid 3743) Sat Nov 26 08:39:31 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 3000
/tmp/isabelle-gene/process7458968389934499957/cache-io-3953942")
ERROR: apport (pid 3743) Sat Nov 26 08:39:31 2016: debug: session gdbus call: (true,)
ERROR: apport (pid 3743) Sat Nov 26 08:39:31 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3753) Sat Nov 26 08:39:32 2016: called for pid 3752, signal 6, core limit 0
ERROR: apport (pid 3753) Sat Nov 26 08:39:32 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 1071
/tmp/isabelle-gene/process7458968389934499957/cache-io-3954988")
ERROR: apport (pid 3753) Sat Nov 26 08:39:32 2016: debug: session gdbus call: (true,)
ERROR: apport (pid 3753) Sat Nov 26 08:39:32 2016: this executable already crashed 2 times, ignoring
Email Gateway (Aug 22 2022 at 14:32):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Eugene, Makarius,
First, thank you, Eugene, for taking the time to reproduce the issue.
Makarius wrote:
Shall we hand this over to the cvc4 guys? There might be still enough
time for our release, to get a clarification of this important fine point.
Indeed. I'll write to them right now on the CVC4 users mailing list. Indeed, I should have done so long ago.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 14:32):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I decided to try replacing the cvc4 binary by a shell script that
ran cvc4 using the "strace" utility. I recorded the attached
trace (edited, original was 13MB long). It seems to show a "normal"
termination of cvc4 by the receipt of SIGINT, which then results
in a call to abort() from the SIGINT handler:
strace_cvc4.digest
Email Gateway (Aug 22 2022 at 14:32):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Eugene,
Aha ! This shows that passing "--no-statistics" to CVC4 is enough to disable this behavior. I'll prepare a changeset for RC2 and send it to Makarius.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 14:33):From: Makarius <makarius@sketis.net>
OK, the change is here
https://bitbucket.org/isabelle_project/isabelle-release/commits/be149db8207a36
and thus scheduled for the next release candidate.
Here is also a document about signal handlers in C:
https://docs.oracle.com/cd/E19455-01/806-5257/gen-26/index.html
High-level things like printf are not allowed, so the above fprintf
might cause problems again at some point. E prover used to have similar
problems some years ago.
For the Isabelle2016-1 the present workaround should be OK, but the CVC4
guys should be informed about these inherent weaknesses of the signal
handlers.
Makarius
Email Gateway (Aug 22 2022 at 14:50):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Eugene,
On 26.11.2016, at 20:37, Eugene W. Stark <isabelle-users@starkeffect.com> wrote:
Unfortunately, the --no-statistics option does not work to suppress the aborts.
That's a pity. Looking at the code, I was overly confident this would do the trick. Regardless, I had filed a bug report to the CVC4 developers and have now updated it:
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=767
There's also a thread on the CVC-USERS mailing list that discussed the issue. To summarize the thread, CVC4 developer Tim King wrote
But if users want an alternative nice death, i.e. exit with a non-zero
code, we might be able to support that. It would probably need to come in
the form of a compile time flag.
And user Johannes Kanig wrote
we (the AdaCore SPARK team, heavy users of cvc4) would definitely welcome such a compile time flag.
I'm sorry we don't have a better resolution for Isabelle2016-1, but we're very much dependent on the CVC4 developers cleaning up their act.
Cheers,
Jasmin
Last updated: Apr 27 2024 at 01:05 UTC