mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix for spurious wakeups in scoped_timer (#6102)

Browse source
This commit is contained in:
Felix Kohlgrüber 2022-06-22 11:50:19 +02:00 committed by GitHub
parent 41deed59a3
commit a7b41c49fe
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 16 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/util/scoped_timer.cpp
View file

@ -80,27 +80,20 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {
return; return;
workers.lock(); workers.lock();
bool new_worker = false;
if (available_workers.empty()) { if (available_workers.empty()) {
// start new thead
workers.unlock(); workers.unlock();
s = new scoped_timer_state; s = new scoped_timer_state;
new_worker = true;
++num_workers; ++num_workers;
s->work = WORKING; init_state(ms, eh);
}
else {
s = available_workers.back();
available_workers.pop_back();
s->work = WORKING;
workers.unlock();
}
s->ms = ms;
s->eh = eh;
s->m_mutex.lock();
if (new_worker) {
s->m_thread = std::thread(thread_func, s); s->m_thread = std::thread(thread_func, s);
} }
else { else {
// re-use existing thread
s = available_workers.back();
available_workers.pop_back();
init_state(ms, eh);
workers.unlock();
s->cv.notify_one(); s->cv.notify_one();
} }
} }
@ -148,3 +141,10 @@ void scoped_timer::finalize() {
num_workers = 0; num_workers = 0;
available_workers.clear(); available_workers.clear();
} }
void scoped_timer::init_state(unsigned ms, event_handler * eh) {
s->ms = ms;
s->eh = eh;
s->m_mutex.lock();
s->work = WORKING;
}

2
src/util/scoped_timer.h
View file

@ -29,6 +29,8 @@ public:
~scoped_timer(); ~scoped_timer();
static void initialize(); static void initialize();
static void finalize(); static void finalize();
private:
void init_state(unsigned ms, event_handler * eh);
}; };
/* /*