[isabelle] z3 crashing, too (was Re: cvc4 crashing)



(In Isabelle2016-1-RC1)
This is maybe unrelated to the cvc4 issue, since this crash is with SIGSEGV.

							- Gene Stark


ProblemType: Crash
Architecture: amd64
CrashCounter: 1
CurrentDesktop: Unity
Date: Thu Nov  3 04:46:21 2016
DistroRelease: Ubuntu 16.04
ExecutablePath: /opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3
ExecutableTimestamp: 1428507126
ProcCmdline: /opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3 smt.random_seed 1 smt.refine_inj_axioms false
-T 1 -smt2 /tmp/isabelle-gene/process3970109973954785755/cache-io-27359710
ProcCwd: /home/gene
ProcEnviron:
 SHELL=/bin/tcsh
 TERM=xterm-256color
 LD_LIBRARY_PATH=<set>
 PATH=(custom, no user)
 LANG=en_US.UTF-8
 LANGUAGE=en_US
 XDG_RUNTIME_DIR=<set>
ProcMaps:
 00400000-0114e000 r-xp 00000000 fc:00 677391
/opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3
 0134d000-01371000 r--p 00d4d000 fc:00 677391
/opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3
 01371000-01373000 rw-p 00d71000 fc:00 677391
/opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3
 01373000-01375000 rw-p 00000000 00:00 0
 02c22000-02e85000 rw-p 00000000 00:00 0                                  [heap]
 7f647c220000-7f647c223000 r-xp 00000000 fc:00 1180234                    /lib/x86_64-linux-gnu/libdl-2.23.so
 7f647c223000-7f647c422000 ---p 00003000 fc:00 1180234                    /lib/x86_64-linux-gnu/libdl-2.23.so
 7f647c422000-7f647c423000 r--p 00002000 fc:00 1180234                    /lib/x86_64-linux-gnu/libdl-2.23.so
 7f647c423000-7f647c424000 rw-p 00003000 fc:00 1180234                    /lib/x86_64-linux-gnu/libdl-2.23.so
 7f647c424000-7f647c5e4000 r-xp 00000000 fc:00 1180232                    /lib/x86_64-linux-gnu/libc-2.23.so
 7f647c5e4000-7f647c7e3000 ---p 001c0000 fc:00 1180232                    /lib/x86_64-linux-gnu/libc-2.23.so
 7f647c7e3000-7f647c7e7000 r--p 001bf000 fc:00 1180232                    /lib/x86_64-linux-gnu/libc-2.23.so
 7f647c7e7000-7f647c7e9000 rw-p 001c3000 fc:00 1180232                    /lib/x86_64-linux-gnu/libc-2.23.so
 7f647c7e9000-7f647c7ed000 rw-p 00000000 00:00 0
 7f647c7ed000-7f647c803000 r-xp 00000000 fc:00 1179781                    /lib/x86_64-linux-gnu/libgcc_s.so.1
 7f647c803000-7f647ca02000 ---p 00016000 fc:00 1179781                    /lib/x86_64-linux-gnu/libgcc_s.so.1
 7f647ca02000-7f647ca03000 rw-p 00015000 fc:00 1179781                    /lib/x86_64-linux-gnu/libgcc_s.so.1
 7f647ca03000-7f647ca24000 r-xp 00000000 fc:00 789048                     /usr/lib/x86_64-linux-gnu/libgomp.so.1.0.0
 7f647ca24000-7f647cc23000 ---p 00021000 fc:00 789048                     /usr/lib/x86_64-linux-gnu/libgomp.so.1.0.0
 7f647cc23000-7f647cc24000 r--p 00020000 fc:00 789048                     /usr/lib/x86_64-linux-gnu/libgomp.so.1.0.0
 7f647cc24000-7f647cc25000 rw-p 00021000 fc:00 789048                     /usr/lib/x86_64-linux-gnu/libgomp.so.1.0.0
 7f647cc25000-7f647cd2d000 r-xp 00000000 fc:00 1180210                    /lib/x86_64-linux-gnu/libm-2.23.so
 7f647cd2d000-7f647cf2c000 ---p 00108000 fc:00 1180210                    /lib/x86_64-linux-gnu/libm-2.23.so
 7f647cf2c000-7f647cf2d000 r--p 00107000 fc:00 1180210                    /lib/x86_64-linux-gnu/libm-2.23.so
 7f647cf2d000-7f647cf2e000 rw-p 00108000 fc:00 1180210                    /lib/x86_64-linux-gnu/libm-2.23.so
 7f647cf2e000-7f647d0a0000 r-xp 00000000 fc:00 788013                     /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.21
 7f647d0a0000-7f647d2a0000 ---p 00172000 fc:00 788013                     /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.21
 7f647d2a0000-7f647d2aa000 r--p 00172000 fc:00 788013                     /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.21
 7f647d2aa000-7f647d2ac000 rw-p 0017c000 fc:00 788013                     /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.21
 7f647d2ac000-7f647d2b0000 rw-p 00000000 00:00 0
 7f647d2b0000-7f647d2b7000 r-xp 00000000 fc:00 1180220                    /lib/x86_64-linux-gnu/librt-2.23.so
 7f647d2b7000-7f647d4b6000 ---p 00007000 fc:00 1180220                    /lib/x86_64-linux-gnu/librt-2.23.so
 7f647d4b6000-7f647d4b7000 r--p 00006000 fc:00 1180220                    /lib/x86_64-linux-gnu/librt-2.23.so
 7f647d4b7000-7f647d4b8000 rw-p 00007000 fc:00 1180220                    /lib/x86_64-linux-gnu/librt-2.23.so
 7f647d4b8000-7f647d4d0000 r-xp 00000000 fc:00 1180230                    /lib/x86_64-linux-gnu/libpthread-2.23.so
 7f647d4d0000-7f647d6cf000 ---p 00018000 fc:00 1180230                    /lib/x86_64-linux-gnu/libpthread-2.23.so
 7f647d6cf000-7f647d6d0000 r--p 00017000 fc:00 1180230                    /lib/x86_64-linux-gnu/libpthread-2.23.so
 7f647d6d0000-7f647d6d1000 rw-p 00018000 fc:00 1180230                    /lib/x86_64-linux-gnu/libpthread-2.23.so
 7f647d6d1000-7f647d6d5000 rw-p 00000000 00:00 0
 7f647d6d5000-7f647d6fb000 r-xp 00000000 fc:00 1180224                    /lib/x86_64-linux-gnu/ld-2.23.so
 7f647d8a3000-7f647d8d3000 rw-p 00000000 00:00 0
 7f647d8f0000-7f647d8f1000 ---p 00000000 00:00 0
 7f647d8f1000-7f647d8fa000 rw-p 00000000 00:00 0
 7f647d8fa000-7f647d8fb000 r--p 00025000 fc:00 1180224                    /lib/x86_64-linux-gnu/ld-2.23.so
 7f647d8fb000-7f647d8fc000 rw-p 00026000 fc:00 1180224                    /lib/x86_64-linux-gnu/ld-2.23.so
 7f647d8fc000-7f647d8fd000 rw-p 00000000 00:00 0
 7fff06fb5000-7fff06fd9000 rw-p 00000000 00:00 0                          [stack]
 7fff06fec000-7fff06fee000 r--p 00000000 00:00 0                          [vvar]
 7fff06fee000-7fff06ff0000 r-xp 00000000 00:00 0                          [vdso]
 ffffffffff600000-ffffffffff601000 r-xp 00000000 00:00 0                  [vsyscall]
ProcStatus:
 Name:	z3
 State:	S (sleeping)
 Tgid:	15560
 Ngid:	0
 Pid:	15560
 PPid:	15559
 TracerPid:	0
 Uid:	1000	1000	1000	1000
 Gid:	1000	1000	1000	1000
 FDSize:	64
 Groups:	4 20 24 27 30 46 112 124 135 1000
 NStgid:	15560
 NSpid:	15560
 NSpgid:	15558
 NSsid:	15558
 VmPeak:	   37992 kB
 VmSize:	   37992 kB
 VmLck:	       0 kB
 VmPin:	       0 kB
 VmHWM:	   16324 kB
 VmRSS:	   16324 kB
 VmData:	    2752 kB
 VmStk:	     148 kB
 VmExe:	   13624 kB
 VmLib:	    4836 kB
 VmPTE:	      84 kB
 VmPMD:	      12 kB
 VmSwap:	       0 kB
 HugetlbPages:	       0 kB
 Threads:	2
 SigQ:	1/95164
 SigPnd:	0000000000000000
 ShdPnd:	0000000000000000
 SigBlk:	0000000000000000
 SigIgn:	0000000000001000
 SigCgt:	0000000180000002
 CapInh:	0000000000000000
 CapPrm:	0000000000000000
 CapEff:	0000000000000000
 CapBnd:	0000003fffffffff
 CapAmb:	0000000000000000
 Seccomp:	0
 Cpus_allowed:	f
 Cpus_allowed_list:	0-3
 Mems_allowed:	00000000,00000001
 Mems_allowed_list:	0
 voluntary_ctxt_switches:	3
 nonvoluntary_ctxt_switches:	11
Signal: 11
Uname: Linux 4.4.0-45-generic x86_64
UserGroups: adm cdrom dialout dip lpadmin plugdev sambashare sudo vboxusers
_LogindSession: c2




On 11/02/2016 10:15 AM, Makarius wrote:
> 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.