Crashes in a multithreaded program on Ctrl-C

[mikulas-patocka]

The object scoped_ctrl_c in src/util/scoped_ctrl_c.cpp is not thread safe. It uses a global variable g_obj without any locking. It installs a signal handler with the "signal" function, but the handler is per-process, not per-thread, so different threads step over each other's handlers. Note also that in a multithreaded program, it is unpredictable which thread receives the signal, so the signal handler may be racing with the compute thread that installed the handler.

I created a program that spawns 16 threads, each thread repeatedly makes a context, fills the context with simple assertions, calls "(check-sat)" and destroys the context. It works reliably, but when Ctrl-C is pressed, I get occasional crashes. The crashes happen inside the "on_ctrl_c" function.

I locked the calls to "Z3_mk_context" and "Z3_del_context" (so that they are not performed in parallel). But I did not lock the calls to "Z3_eval_smtlib2_string" because they are done on different contexts. Note that calling "Z3_eval_smtlib2_string" from only one thread wouldn't fix this bug entirely, because the signal handler may be run in a different thread and may race with scoped_ctrl_c destructor.

[NikolajBjorner]

scoped_ctrl_c.cpp can be rewritten using C++ atomic and atomic compare and swap in several places.

[mikulas-patocka]

I have created a pull request for this: #7608

[NikolajBjorner]

@nunoplopes

[nunoplopes]

(I'm taking off for vacations next week. I'll come back to this in August)