mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix deadlock in scoped_timer destructor (#5371)

Browse source
This commit is contained in:
zhouzhenghui 2021-12-22 02:47:13 +08:00 • committed by GitHub
parent 94a2c91f39
commit 9d82c1d8a9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/util/scoped_timer.cpp
View file

@ -33,12 +33,14 @@ Revision History:
#include <pthread.h>
#endif
enum scoped_timer_work_state { IDLE = 0, WORKING = 1, EXITING = 2 };
struct scoped_timer_state {
std::thread m_thread;
std::timed_mutex m_mutex;
event_handler * eh;
unsigned ms;
std::atomic<int> work;
std::atomic<scoped_timer_work_state> work;
std::condition_variable_any cv;
};
@ -49,11 +51,11 @@ static atomic<unsigned> num_workers(0);
static void thread_func(scoped_timer_state *s) {
workers.lock();
while (true) {
s->cv.wait(workers, [=]{ return s->work > 0; });
s->cv.wait(workers, [=]{ return s->work > IDLE; });
workers.unlock();
// exiting..
if (s->work == 2)
if (s->work == EXITING)
return;
auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(s->ms);
@ -68,9 +70,8 @@ static void thread_func(scoped_timer_state *s) {
s->m_mutex.unlock();
next:
s->work = 0;
s->work = IDLE;
workers.lock();
available_workers.push_back(s);
}
}
@ -97,7 +98,7 @@ public:
s->ms = ms;
s->eh = eh;
s->m_mutex.lock();
s->work = 1;
s->work = WORKING;
if (new_worker) {
s->m_thread = std::thread(thread_func, s);
}
@ -108,8 +109,11 @@ public:
~imp() {
s->m_mutex.unlock();
while (s->work == 1)
while (s->work == WORKING)
std::this_thread::yield();
workers.lock();
available_workers.push_back(s);
workers.unlock();
}
};
@ -139,7 +143,7 @@ void scoped_timer::finalize() {
while (deleted < num_workers) {
workers.lock();
for (auto w : available_workers) {
w->work = 2;
w->work = EXITING;
w->cv.notify_one();
}
decltype(available_workers) cleanup_workers;