Re: [isabelle] cvc4 crashing



On 29/10/16 12:07, Eugene W. Stark wrote:
> I can report that cvc4 has crashed in the same way under Isabelle2016-RC1
> running on Ubuntu 16.04 LTS on the amd64 architecture.  I have appended the
> Ubuntu crash report (minus the core dump).
> 
> It looks to me like the cvc4 process is sleeping at the time it receives
> a SIGABRT, which causes abnormal termination.  I'm not quite sure why a
> process would receive a SIGABRT while it is sleeping, unless for some
> reason that is a mechanism being used to forcibly terminate the process.
> If that is the case, perhaps there is some situation (due to the interaction
> of some library code with the signal mechanism) under which the cvc4 process
> can enter the kernel with the SIGABRT handler disabled, so that if the signal
> happens to be delivered during that time the default action (core dump)
> will occur.

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.