mirror of
https://github.com/Z3Prover/z3
synced 2025-08-03 09:50:23 +00:00
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 <mikulas@twibright.com>
This commit is contained in:
parent
bb81f26fcb
commit
88eb4634d0
3 changed files with 26 additions and 5 deletions
|
@ -18,28 +18,46 @@ Revision History:
|
||||||
--*/
|
--*/
|
||||||
#pragma once
|
#pragma once
|
||||||
|
|
||||||
|
#include <atomic>
|
||||||
#include "util/event_handler.h"
|
#include "util/event_handler.h"
|
||||||
|
#include "util/scoped_ctrl_c.h"
|
||||||
|
|
||||||
/**
|
/**
|
||||||
\brief Generic event handler for invoking cancel method.
|
\brief Generic event handler for invoking cancel method.
|
||||||
*/
|
*/
|
||||||
template<typename T>
|
template<typename T>
|
||||||
class cancel_eh : public event_handler {
|
class cancel_eh : public event_handler {
|
||||||
bool m_canceled = false;
|
std::atomic<bool> m_canceled = false;
|
||||||
bool m_auto_cancel = false;
|
bool m_auto_cancel = false;
|
||||||
T & m_obj;
|
T & m_obj;
|
||||||
public:
|
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();
|
||||||
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();
|
||||||
|
}
|
||||||
|
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; }
|
T& t() { return m_obj; }
|
||||||
void set_auto_cancel() { m_auto_cancel = true; }
|
void set_auto_cancel() { m_auto_cancel = true; }
|
||||||
};
|
};
|
||||||
|
|
|
@ -36,7 +36,7 @@ static struct sigaction old_sigaction;
|
||||||
#endif
|
#endif
|
||||||
static bool signal_handled = false;
|
static bool signal_handled = false;
|
||||||
|
|
||||||
static void signal_lock(void) {
|
void signal_lock(void) {
|
||||||
#ifdef USE_SIGNAL
|
#ifdef USE_SIGNAL
|
||||||
context_lock.lock();
|
context_lock.lock();
|
||||||
#else
|
#else
|
||||||
|
@ -50,7 +50,7 @@ static void signal_lock(void) {
|
||||||
#endif
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
static void signal_unlock(void) {
|
void signal_unlock(void) {
|
||||||
#ifdef USE_SIGNAL
|
#ifdef USE_SIGNAL
|
||||||
context_lock.unlock();
|
context_lock.unlock();
|
||||||
#else
|
#else
|
||||||
|
|
|
@ -21,6 +21,9 @@ Revision History:
|
||||||
#include "util/event_handler.h"
|
#include "util/event_handler.h"
|
||||||
#include "util/util.h"
|
#include "util/util.h"
|
||||||
|
|
||||||
|
void signal_lock(void);
|
||||||
|
void signal_unlock(void);
|
||||||
|
|
||||||
struct scoped_ctrl_c {
|
struct scoped_ctrl_c {
|
||||||
event_handler & m_cancel_eh;
|
event_handler & m_cancel_eh;
|
||||||
bool m_first;
|
bool m_first;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue