The Ctrl-C handling is not thread safe, there's a global variable g_obj
that is being accessed without any locking. The signal handlers are
per-process, not per-thread, so that different threads step over each
other's handlers. It is unpredictable in which thread the signal handler
runs, so the handler may race with the scoped_ctrl_c destructor.
Fix this by introducing the functions signal_lock and signal_unlock.
signal_lock blocks the SIGINT signal and then takes a mutex (so that the
signal handler can't be called while the mutex is held). signal_unlock
drops the mutex and restores the signal mask.
We protect all the global variables with signal_lock and signal_unlock.
Note that on Windows, the SIGINT handler is being run in a separate
thread (and there is no way how to block it), so we can use a simple
mutex to synchronize the signal handler with the other threads.
In class cancel_eh, the operator () may be called concurrently by the
timer code and the Ctrl-C code, but the operator () accesses class'
members without any locking. Fix this race condition by using the
functions signal_lock() and signal_unlock().
There is this possible call trace:
SIGINT signal
on_sigint
a->m_cancel_eh()
cancel_eh::operator()
m_obj.inc_cancel
reslimit::inc_cancel
lock_guard lock(*g_rlimit_mux);
Here we take a mutex from a signal - this is subject to deadlock (if the
signal interrupted another piece of code where the mutex is already
held).
To fix this race, we remove g_rlimit_mux and replace it with
signal_lock() and signal_unlock(). signal_lock and signal_unlock block
the signal before grabbing the mutex, so the signal can't interrupt a
piece of code where the mutex is held and the deadlock won't happen.
Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM.
Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers.
The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time.
We characterize it as based on polling.
