mirror of
https://github.com/Z3Prover/z3
synced 2025-08-02 09:20:22 +00:00
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 <mikulas@twibright.com>
This commit is contained in:
parent
88eb4634d0
commit
a4e7bf82da
3 changed files with 35 additions and 23 deletions
|
@ -34,14 +34,12 @@ public:
|
||||||
cancel_eh(T & o): m_obj(o) {}
|
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(); }
|
~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 {
|
void operator()(event_handler_caller_t caller_id) override {
|
||||||
if (caller_id != CTRL_C_EH_CALLER)
|
|
||||||
signal_lock();
|
signal_lock();
|
||||||
if (!m_canceled) {
|
if (!m_canceled) {
|
||||||
m_caller_id = caller_id;
|
m_caller_id = caller_id;
|
||||||
m_canceled = true;
|
m_canceled = true;
|
||||||
m_obj.inc_cancel();
|
m_obj.inc_cancel();
|
||||||
}
|
}
|
||||||
if (caller_id != CTRL_C_EH_CALLER)
|
|
||||||
signal_unlock();
|
signal_unlock();
|
||||||
}
|
}
|
||||||
bool canceled() {
|
bool canceled() {
|
||||||
|
|
|
@ -19,16 +19,12 @@ Revision History:
|
||||||
#include "util/rlimit.h"
|
#include "util/rlimit.h"
|
||||||
#include "util/common_msgs.h"
|
#include "util/common_msgs.h"
|
||||||
#include "util/mutex.h"
|
#include "util/mutex.h"
|
||||||
|
#include "util/scoped_ctrl_c.h"
|
||||||
|
|
||||||
static DECLARE_MUTEX(g_rlimit_mux);
|
|
||||||
|
|
||||||
void initialize_rlimit() {
|
void initialize_rlimit() {
|
||||||
ALLOC_MUTEX(g_rlimit_mux);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void finalize_rlimit() {
|
void finalize_rlimit() {
|
||||||
DEALLOC_MUTEX(g_rlimit_mux);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
reslimit::reslimit() {
|
reslimit::reslimit() {
|
||||||
|
@ -77,57 +73,66 @@ char const* reslimit::get_cancel_msg() const {
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::push_child(reslimit* r) {
|
void reslimit::push_child(reslimit* r) {
|
||||||
lock_guard lock(*g_rlimit_mux);
|
signal_lock();
|
||||||
m_children.push_back(r);
|
m_children.push_back(r);
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::pop_child() {
|
void reslimit::pop_child() {
|
||||||
lock_guard lock(*g_rlimit_mux);
|
signal_lock();
|
||||||
m_count += m_children.back()->m_count;
|
m_count += m_children.back()->m_count;
|
||||||
m_children.back()->m_count = 0;
|
m_children.back()->m_count = 0;
|
||||||
m_children.pop_back();
|
m_children.pop_back();
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::pop_child(reslimit* r) {
|
void reslimit::pop_child(reslimit* r) {
|
||||||
lock_guard lock(*g_rlimit_mux);
|
signal_lock();
|
||||||
for (unsigned i = 0; i < m_children.size(); ++i) {
|
for (unsigned i = 0; i < m_children.size(); ++i) {
|
||||||
if (m_children[i] == r) {
|
if (m_children[i] == r) {
|
||||||
m_count += r->m_count;
|
m_count += r->m_count;
|
||||||
r->m_count = 0;
|
r->m_count = 0;
|
||||||
m_children.erase(m_children.begin() + i);
|
m_children.erase(m_children.begin() + i);
|
||||||
return;
|
break;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
void reslimit::cancel() {
|
void reslimit::cancel() {
|
||||||
lock_guard lock(*g_rlimit_mux);
|
signal_lock();
|
||||||
set_cancel(m_cancel+1);
|
set_cancel(m_cancel+1);
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::reset_cancel() {
|
void reslimit::reset_cancel() {
|
||||||
lock_guard lock(*g_rlimit_mux);
|
signal_lock();
|
||||||
set_cancel(0);
|
set_cancel(0);
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::inc_cancel() {
|
void reslimit::inc_cancel() {
|
||||||
lock_guard lock(*g_rlimit_mux);
|
signal_lock();
|
||||||
set_cancel(m_cancel + 1);
|
set_cancel(m_cancel + 1);
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::dec_cancel() {
|
void reslimit::dec_cancel() {
|
||||||
lock_guard lock(*g_rlimit_mux);
|
signal_lock();
|
||||||
if (m_cancel > 0) {
|
if (m_cancel > 0) {
|
||||||
set_cancel(m_cancel-1);
|
set_cancel(m_cancel-1);
|
||||||
}
|
}
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::set_cancel(unsigned f) {
|
void reslimit::set_cancel(unsigned f) {
|
||||||
|
signal_lock();
|
||||||
m_cancel = f;
|
m_cancel = f;
|
||||||
for (unsigned i = 0; i < m_children.size(); ++i) {
|
for (unsigned i = 0; i < m_children.size(); ++i) {
|
||||||
m_children[i]->set_cancel(f);
|
m_children[i]->set_cancel(f);
|
||||||
}
|
}
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@ -151,8 +156,9 @@ void reslimit::push_timeout(unsigned ms) {
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::inc_cancel(unsigned k) {
|
void reslimit::inc_cancel(unsigned k) {
|
||||||
lock_guard lock(*g_rlimit_mux);
|
signal_lock();
|
||||||
set_cancel(m_cancel + k);
|
set_cancel(m_cancel + k);
|
||||||
|
signal_unlock();
|
||||||
}
|
}
|
||||||
|
|
||||||
void reslimit::auto_cancel() {
|
void reslimit::auto_cancel() {
|
||||||
|
|
|
@ -26,13 +26,14 @@ Revision History:
|
||||||
#define USE_SIGNAL
|
#define USE_SIGNAL
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
static std::mutex context_lock;
|
static std::recursive_mutex context_lock;
|
||||||
static std::vector<scoped_ctrl_c *> active_contexts;
|
static std::vector<scoped_ctrl_c *> active_contexts;
|
||||||
#ifdef USE_SIGNAL
|
#ifdef USE_SIGNAL
|
||||||
static void (*old_handler)(int);
|
static void (*old_handler)(int);
|
||||||
#else
|
#else
|
||||||
static sigset_t context_old_set;
|
static sigset_t context_old_set;
|
||||||
static struct sigaction old_sigaction;
|
static struct sigaction old_sigaction;
|
||||||
|
static unsigned signal_lock_depth = 0;
|
||||||
#endif
|
#endif
|
||||||
static bool signal_handled = false;
|
static bool signal_handled = false;
|
||||||
|
|
||||||
|
@ -46,6 +47,8 @@ void signal_lock(void) {
|
||||||
if (sigprocmask(SIG_BLOCK, &set, &old_set))
|
if (sigprocmask(SIG_BLOCK, &set, &old_set))
|
||||||
abort();
|
abort();
|
||||||
context_lock.lock();
|
context_lock.lock();
|
||||||
|
signal_lock_depth++;
|
||||||
|
if (signal_lock_depth == 1)
|
||||||
context_old_set = old_set;
|
context_old_set = old_set;
|
||||||
#endif
|
#endif
|
||||||
}
|
}
|
||||||
|
@ -54,10 +57,15 @@ void signal_unlock(void) {
|
||||||
#ifdef USE_SIGNAL
|
#ifdef USE_SIGNAL
|
||||||
context_lock.unlock();
|
context_lock.unlock();
|
||||||
#else
|
#else
|
||||||
|
bool restore;
|
||||||
sigset_t old_set = context_old_set;
|
sigset_t old_set = context_old_set;
|
||||||
|
signal_lock_depth--;
|
||||||
|
restore = !signal_lock_depth;
|
||||||
context_lock.unlock();
|
context_lock.unlock();
|
||||||
|
if (restore) {
|
||||||
if (sigprocmask(SIG_SETMASK, &old_set, NULL))
|
if (sigprocmask(SIG_SETMASK, &old_set, NULL))
|
||||||
abort();
|
abort();
|
||||||
|
}
|
||||||
#endif
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue