mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

fix #5990: deadlock in the scoped_timer

Browse source 
Thanks to Felix Kohlgrueber for reporting the bug and for the analysis
This commit is contained in:
Nuno Lopes 2022-06-21 16:29:09 +01:00
parent 911134b3c7
commit 25e915fe95
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/util/scoped_timer.cpp
View file

@ -51,10 +51,9 @@ static atomic<unsigned> num_workers(0);
static void thread_func(scoped_timer_state *s) { static void thread_func(scoped_timer_state *s) {
workers.lock(); workers.lock();
while (true) { while (true) {
s->cv.wait(workers, [=]{ return s->work > IDLE; }); s->cv.wait(workers, [=]{ return s->work != IDLE; });
workers.unlock(); workers.unlock();
// exiting..
if (s->work == EXITING) if (s->work == EXITING)
return; return;
@ -87,16 +86,17 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {
s = new scoped_timer_state; s = new scoped_timer_state;
new_worker = true; new_worker = true;
++num_workers; ++num_workers;
s->work = WORKING;
} }
else { else {
s = available_workers.back(); s = available_workers.back();
available_workers.pop_back(); available_workers.pop_back();
s->work = WORKING;
workers.unlock(); workers.unlock();
} }
s->ms = ms; s->ms = ms;
s->eh = eh; s->eh = eh;
s->m_mutex.lock(); s->m_mutex.lock();
s->work = WORKING;
if (new_worker) { if (new_worker) {
s->m_thread = std::thread(thread_func, s); s->m_thread = std::thread(thread_func, s);
} }