From bb81f26fcb6c99ac3a81cd6f4d511e6d8f4e0029 Mon Sep 17 00:00:00 2001 From: Mikulas Patocka Date: Sun, 6 Apr 2025 19:10:19 +0200 Subject: [PATCH 1/5] Make Ctrl-C handling thread-safe (#7603) 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. Signed-off-by: Mikulas Patocka --- src/util/scoped_ctrl_c.cpp | 121 ++++++++++++++++++++++++++++++------- src/util/scoped_ctrl_c.h | 2 - 2 files changed, 100 insertions(+), 23 deletions(-) diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index a3f5ee772..5d1700823 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -12,46 +12,125 @@ Abstract: Author: Leonardo de Moura (leonardo) 2011-04-27. + Mikulas Patocka 2025-04-05. (rewritten to be thread safe) Revision History: --*/ -#include +#include +#include +#include #include "util/scoped_ctrl_c.h" -static scoped_ctrl_c * g_obj = nullptr; +#ifdef _WINDOWS +#define USE_SIGNAL +#endif -static void on_ctrl_c(int) { - if (g_obj->m_first) { - g_obj->m_cancel_eh(CTRL_C_EH_CALLER); - if (g_obj->m_once) { - g_obj->m_first = false; - signal(SIGINT, on_ctrl_c); // re-install the handler - } +static std::mutex context_lock; +static std::vector active_contexts; +#ifdef USE_SIGNAL +static void (*old_handler)(int); +#else +static sigset_t context_old_set; +static struct sigaction old_sigaction; +#endif +static bool signal_handled = false; + +static void signal_lock(void) { +#ifdef USE_SIGNAL + context_lock.lock(); +#else + sigset_t set, old_set; + sigemptyset(&set); + sigaddset(&set, SIGINT); + if (sigprocmask(SIG_BLOCK, &set, &old_set)) + abort(); + context_lock.lock(); + context_old_set = old_set; +#endif +} + +static void signal_unlock(void) { +#ifdef USE_SIGNAL + context_lock.unlock(); +#else + sigset_t old_set = context_old_set; + context_lock.unlock(); + if (sigprocmask(SIG_SETMASK, &old_set, NULL)) + abort(); +#endif +} + +static void test_and_unhandle(void) { + if (!signal_handled) + return; + for (auto a : active_contexts) { + if (a->m_first) + return; } - else { - signal(SIGINT, g_obj->m_old_handler); - raise(SIGINT); +#ifdef USE_SIGNAL + signal(SIGINT, old_handler); +#else + if (sigaction(SIGINT, &old_sigaction, NULL)) + abort(); +#endif + signal_handled = false; +} + +static void on_sigint(int) { + signal_lock(); +#ifdef USE_SIGNAL + if (signal_handled) + signal(SIGINT, on_sigint); +#endif + for (auto a : active_contexts) { + if (a->m_first) + a->m_cancel_eh(CTRL_C_EH_CALLER); + if (a->m_once) + a->m_first = false; } + test_and_unhandle(); + signal_unlock(); } scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool once, bool enabled): - m_cancel_eh(eh), + m_cancel_eh(eh), m_first(true), m_once(once), - m_enabled(enabled), - m_old_scoped_ctrl_c(g_obj) { + m_enabled(enabled) { if (m_enabled) { - g_obj = this; - m_old_handler = signal(SIGINT, on_ctrl_c); + signal_lock(); + active_contexts.push_back(this); + if (!signal_handled) { +#ifdef USE_SIGNAL + old_handler = signal(SIGINT, on_sigint); +#else + struct sigaction sa; + memset(&sa, 0, sizeof(struct sigaction)); + sa.sa_handler = on_sigint; + sigemptyset(&sa.sa_mask); + sa.sa_flags = SA_RESTART; + if (sigaction(SIGINT, &sa, &old_sigaction)) + abort(); +#endif + signal_handled = true; + } + signal_unlock(); } } -scoped_ctrl_c::~scoped_ctrl_c() { +scoped_ctrl_c::~scoped_ctrl_c() { if (m_enabled) { - g_obj = m_old_scoped_ctrl_c; - if (m_old_handler != SIG_ERR) { - signal(SIGINT, m_old_handler); + signal_lock(); + for (auto it = active_contexts.begin(); it != active_contexts.end(); it++) { + if (*it == this) { + active_contexts.erase(it); + goto found; + } } + abort(); +found: + test_and_unhandle(); + signal_unlock(); } } diff --git a/src/util/scoped_ctrl_c.h b/src/util/scoped_ctrl_c.h index 09bc55c05..2b67f59a5 100644 --- a/src/util/scoped_ctrl_c.h +++ b/src/util/scoped_ctrl_c.h @@ -26,8 +26,6 @@ struct scoped_ctrl_c { bool m_first; bool m_once; bool m_enabled; - void (STD_CALL *m_old_handler)(int); - scoped_ctrl_c * m_old_scoped_ctrl_c; public: // If once == true, then the cancel_eh is invoked only at the first Ctrl-C. // The next time, the old signal handler will take over. From 88eb4634d08ced416c11c7265ed7dc38a072bf74 Mon Sep 17 00:00:00 2001 From: Mikulas Patocka Date: Sun, 6 Apr 2025 19:10:44 +0200 Subject: [PATCH 2/5] Fix a race condition between timer and Ctrl-C 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() that were introduced in a previous patch. Note that if caller_id is CTRL_C_EH_CALLER, signal_lock was already called by the caller. Note that we must use signal_lock/signal_unlock and we must not grab any other mutex, because the SIGINT signal could interrupt the code while the mutex is held and cause deadlock. Signed-off-by: Mikulas Patocka --- src/util/cancel_eh.h | 24 +++++++++++++++++++++--- src/util/scoped_ctrl_c.cpp | 4 ++-- src/util/scoped_ctrl_c.h | 3 +++ 3 files changed, 26 insertions(+), 5 deletions(-) diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h index d609b957a..23ba5b7dc 100644 --- a/src/util/cancel_eh.h +++ b/src/util/cancel_eh.h @@ -18,28 +18,46 @@ Revision History: --*/ #pragma once +#include #include "util/event_handler.h" +#include "util/scoped_ctrl_c.h" /** \brief Generic event handler for invoking cancel method. */ template class cancel_eh : public event_handler { - bool m_canceled = false; + std::atomic m_canceled = false; bool m_auto_cancel = false; T & m_obj; public: cancel_eh(T & o): m_obj(o) {} ~cancel_eh() override { if (m_canceled) m_obj.dec_cancel(); if (m_auto_cancel) m_obj.auto_cancel(); } void operator()(event_handler_caller_t caller_id) override { + if (caller_id != CTRL_C_EH_CALLER) + signal_lock(); if (!m_canceled) { m_caller_id = caller_id; m_canceled = true; m_obj.inc_cancel(); } + if (caller_id != CTRL_C_EH_CALLER) + signal_unlock(); + } + bool canceled() { + bool ret; + if (!m_canceled) + return false; + signal_lock(); + ret = m_canceled; + signal_unlock(); + return ret; + } + void reset() { + signal_lock(); + m_canceled = false; + signal_unlock(); } - bool canceled() const { return m_canceled; } - void reset() { m_canceled = false; } T& t() { return m_obj; } void set_auto_cancel() { m_auto_cancel = true; } }; diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index 5d1700823..0ca15eaa9 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -36,7 +36,7 @@ static struct sigaction old_sigaction; #endif static bool signal_handled = false; -static void signal_lock(void) { +void signal_lock(void) { #ifdef USE_SIGNAL context_lock.lock(); #else @@ -50,7 +50,7 @@ static void signal_lock(void) { #endif } -static void signal_unlock(void) { +void signal_unlock(void) { #ifdef USE_SIGNAL context_lock.unlock(); #else diff --git a/src/util/scoped_ctrl_c.h b/src/util/scoped_ctrl_c.h index 2b67f59a5..f686962f4 100644 --- a/src/util/scoped_ctrl_c.h +++ b/src/util/scoped_ctrl_c.h @@ -21,6 +21,9 @@ Revision History: #include "util/event_handler.h" #include "util/util.h" +void signal_lock(void); +void signal_unlock(void); + struct scoped_ctrl_c { event_handler & m_cancel_eh; bool m_first; From a4e7bf82daa19bc4b4dd72a07e8cfa2b68b0e392 Mon Sep 17 00:00:00 2001 From: Mikulas Patocka Date: Sun, 6 Apr 2025 19:11:04 +0200 Subject: [PATCH 3/5] Fix grabbing a mutex from a signal handler 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. We change std::mutex to std::recursive_mutex, so that the mutex can be grabbed multiple times by the same thread. Signed-off-by: Mikulas Patocka --- src/util/cancel_eh.h | 6 ++---- src/util/rlimit.cpp | 36 +++++++++++++++++++++--------------- src/util/scoped_ctrl_c.cpp | 16 ++++++++++++---- 3 files changed, 35 insertions(+), 23 deletions(-) diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h index 23ba5b7dc..792eeb010 100644 --- a/src/util/cancel_eh.h +++ b/src/util/cancel_eh.h @@ -34,15 +34,13 @@ public: cancel_eh(T & o): m_obj(o) {} ~cancel_eh() override { if (m_canceled) m_obj.dec_cancel(); if (m_auto_cancel) m_obj.auto_cancel(); } void operator()(event_handler_caller_t caller_id) override { - if (caller_id != CTRL_C_EH_CALLER) - signal_lock(); + signal_lock(); if (!m_canceled) { m_caller_id = caller_id; m_canceled = true; m_obj.inc_cancel(); } - if (caller_id != CTRL_C_EH_CALLER) - signal_unlock(); + signal_unlock(); } bool canceled() { bool ret; diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index 28656bc63..f73acd200 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -19,16 +19,12 @@ Revision History: #include "util/rlimit.h" #include "util/common_msgs.h" #include "util/mutex.h" - - -static DECLARE_MUTEX(g_rlimit_mux); +#include "util/scoped_ctrl_c.h" void initialize_rlimit() { - ALLOC_MUTEX(g_rlimit_mux); } void finalize_rlimit() { - DEALLOC_MUTEX(g_rlimit_mux); } reslimit::reslimit() { @@ -77,57 +73,66 @@ char const* reslimit::get_cancel_msg() const { } void reslimit::push_child(reslimit* r) { - lock_guard lock(*g_rlimit_mux); + signal_lock(); m_children.push_back(r); + signal_unlock(); } void reslimit::pop_child() { - lock_guard lock(*g_rlimit_mux); + signal_lock(); m_count += m_children.back()->m_count; m_children.back()->m_count = 0; m_children.pop_back(); + signal_unlock(); } void reslimit::pop_child(reslimit* r) { - lock_guard lock(*g_rlimit_mux); + signal_lock(); for (unsigned i = 0; i < m_children.size(); ++i) { if (m_children[i] == r) { m_count += r->m_count; r->m_count = 0; m_children.erase(m_children.begin() + i); - return; + break; } } + signal_unlock(); } void reslimit::cancel() { - lock_guard lock(*g_rlimit_mux); + signal_lock(); set_cancel(m_cancel+1); + signal_unlock(); } void reslimit::reset_cancel() { - lock_guard lock(*g_rlimit_mux); + signal_lock(); set_cancel(0); + signal_unlock(); } void reslimit::inc_cancel() { - lock_guard lock(*g_rlimit_mux); + signal_lock(); set_cancel(m_cancel + 1); + signal_unlock(); } void reslimit::dec_cancel() { - lock_guard lock(*g_rlimit_mux); + signal_lock(); if (m_cancel > 0) { set_cancel(m_cancel-1); } + signal_unlock(); } void reslimit::set_cancel(unsigned f) { + signal_lock(); m_cancel = f; for (unsigned i = 0; i < m_children.size(); ++i) { m_children[i]->set_cancel(f); } + signal_unlock(); } @@ -151,8 +156,9 @@ void reslimit::push_timeout(unsigned ms) { } void reslimit::inc_cancel(unsigned k) { - lock_guard lock(*g_rlimit_mux); + signal_lock(); set_cancel(m_cancel + k); + signal_unlock(); } void reslimit::auto_cancel() { @@ -164,4 +170,4 @@ void reslimit::auto_cancel() { void reslimit::auto_cancel() { UNREACHABLE(); } -#endif \ No newline at end of file +#endif diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index 0ca15eaa9..e5502dc33 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -26,13 +26,14 @@ Revision History: #define USE_SIGNAL #endif -static std::mutex context_lock; +static std::recursive_mutex context_lock; static std::vector active_contexts; #ifdef USE_SIGNAL static void (*old_handler)(int); #else static sigset_t context_old_set; static struct sigaction old_sigaction; +static unsigned signal_lock_depth = 0; #endif static bool signal_handled = false; @@ -46,7 +47,9 @@ void signal_lock(void) { if (sigprocmask(SIG_BLOCK, &set, &old_set)) abort(); context_lock.lock(); - context_old_set = old_set; + signal_lock_depth++; + if (signal_lock_depth == 1) + context_old_set = old_set; #endif } @@ -54,10 +57,15 @@ void signal_unlock(void) { #ifdef USE_SIGNAL context_lock.unlock(); #else + bool restore; sigset_t old_set = context_old_set; + signal_lock_depth--; + restore = !signal_lock_depth; context_lock.unlock(); - if (sigprocmask(SIG_SETMASK, &old_set, NULL)) - abort(); + if (restore) { + if (sigprocmask(SIG_SETMASK, &old_set, NULL)) + abort(); + } #endif } From 95d90a7be515ecb895b2f5a3f265bb2b271a4eca Mon Sep 17 00:00:00 2001 From: Mikulas Patocka Date: Sun, 6 Apr 2025 19:11:29 +0200 Subject: [PATCH 4/5] Fix a race condition in scoped_timer::finalize scoped_timer::finalize is called from fork. However, it may race with other threads creating or freeing timer threads. This patch reworks scoped_timer::finalize so that it runs only once (there is no need to repeat it). We remove the assignments "num_workers = 0" and "available_workers.clear();" - they were done without any locks, thus they were subjects to race condition. The variable num_workers is deleted because it is not needed. There was another bug in scoped_timer::finalize - if some workers were busy, the function would spin-wait for them to terminate. This patch changes it so that busy workers are ignored. Signed-off-by: Mikulas Patocka --- src/util/scoped_timer.cpp | 37 ++++++++++++++----------------------- 1 file changed, 14 insertions(+), 23 deletions(-) diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 4a62b9280..2347132ce 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -48,7 +48,6 @@ struct scoped_timer_state { static std::vector available_workers; static std::mutex workers; -static atomic num_workers(0); static void thread_func(scoped_timer_state *s) { workers.lock(); @@ -94,7 +93,6 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { // start new thead workers.unlock(); s = new scoped_timer_state; - ++num_workers; init_state(ms, eh); s->m_thread = std::thread(thread_func, s); } @@ -122,34 +120,27 @@ scoped_timer::~scoped_timer() { void scoped_timer::initialize() { #ifndef _WINDOWS - static bool pthread_atfork_set = false; - if (!pthread_atfork_set) { + static std::atomic pthread_atfork_set = false; + if (!pthread_atfork_set.exchange(true)) { pthread_atfork(finalize, nullptr, nullptr); - pthread_atfork_set = true; } #endif } void scoped_timer::finalize() { - unsigned deleted = 0; - while (deleted < num_workers) { - workers.lock(); - for (auto w : available_workers) { - w->work = EXITING; - w->cv.notify_one(); - } - decltype(available_workers) cleanup_workers; - std::swap(available_workers, cleanup_workers); - workers.unlock(); - - for (auto w : cleanup_workers) { - ++deleted; - w->m_thread.join(); - delete w; - } + workers.lock(); + for (auto w : available_workers) { + w->work = EXITING; + w->cv.notify_one(); + } + decltype(available_workers) cleanup_workers; + std::swap(available_workers, cleanup_workers); + workers.unlock(); + + for (auto w : cleanup_workers) { + w->m_thread.join(); + delete w; } - num_workers = 0; - available_workers.clear(); } void scoped_timer::init_state(unsigned ms, event_handler * eh) { From a0129539856b8ca321a96c69bf2e0a4106053ab8 Mon Sep 17 00:00:00 2001 From: Mikulas Patocka Date: Sun, 6 Apr 2025 19:11:45 +0200 Subject: [PATCH 5/5] Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling Add this option, so that the z3 library can be used in programs that do signal handling on their own. Signed-off-by: Mikulas Patocka --- src/params/context_params.cpp | 1 + src/util/scoped_ctrl_c.cpp | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index a5c907208..702e0898d 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -157,6 +157,7 @@ void context_params::updt_params(params_ref const & p) { void context_params::collect_param_descrs(param_descrs & d) { insert_rlimit(d); insert_timeout(d); + insert_ctrl_c(d); d.insert("well_sorted_check", CPK_BOOL, "type checker", "false"); d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index e5502dc33..dab994db8 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -20,6 +20,7 @@ Revision History: #include #include #include +#include "util/gparams.h" #include "util/scoped_ctrl_c.h" #ifdef _WINDOWS @@ -106,6 +107,8 @@ scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool once, bool enabled): m_first(true), m_once(once), m_enabled(enabled) { + if (gparams::get_value("ctrl_c") == "false") + m_enabled = false; if (m_enabled) { signal_lock(); active_contexts.push_back(this);