mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
thread pool for scoped_timer (#4748)
creating a fresh thread for every scoped_timer has significant overhead in some use cases. this patch creates a persistent pool of worker threads to do this job, resulting in 20-30% speedup of some alive2 jobs on a large multicore
This commit is contained in:
parent
0c354c7aab
commit
a95c35dadb
|
@ -23,37 +23,82 @@ Revision History:
|
|||
#include "util/util.h"
|
||||
#include <chrono>
|
||||
#include <climits>
|
||||
#include <condition_variable>
|
||||
#include <mutex>
|
||||
#include <thread>
|
||||
#include <vector>
|
||||
|
||||
|
||||
struct scoped_timer::imp {
|
||||
private:
|
||||
std::thread m_thread;
|
||||
struct state {
|
||||
std::thread * m_thread = nullptr;
|
||||
std::timed_mutex m_mutex;
|
||||
unsigned ms;
|
||||
event_handler * eh;
|
||||
int work = 0;
|
||||
std::condition_variable_any cv;
|
||||
};
|
||||
|
||||
static void thread_func(unsigned ms, event_handler * eh, std::timed_mutex * mutex) {
|
||||
auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(ms);
|
||||
/*
|
||||
* NOTE: this implementation deliberately leaks threads when Z3
|
||||
* exits. this is preferable to deallocating on exit, because
|
||||
* destructing threads blocked on condition variables leads to
|
||||
* deadlock.
|
||||
*/
|
||||
static std::vector<state *> available_workers;
|
||||
static std::mutex workers;
|
||||
|
||||
while (!mutex->try_lock_until(end)) {
|
||||
static void thread_func(state *s) {
|
||||
workers.lock();
|
||||
while (true) {
|
||||
s->cv.wait(workers, [=]{ return s->work > 0; });
|
||||
workers.unlock();
|
||||
|
||||
auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(s->ms);
|
||||
|
||||
while (!s->m_mutex.try_lock_until(end)) {
|
||||
if (std::chrono::steady_clock::now() >= end) {
|
||||
eh->operator()(TIMEOUT_EH_CALLER);
|
||||
return;
|
||||
s->eh->operator()(TIMEOUT_EH_CALLER);
|
||||
goto next;
|
||||
}
|
||||
}
|
||||
|
||||
mutex->unlock();
|
||||
s->m_mutex.unlock();
|
||||
|
||||
next:
|
||||
s->work = 0;
|
||||
workers.lock();
|
||||
available_workers.push_back(s);
|
||||
}
|
||||
}
|
||||
|
||||
struct scoped_timer::imp {
|
||||
private:
|
||||
state *s;
|
||||
|
||||
public:
|
||||
imp(unsigned ms, event_handler * eh) {
|
||||
m_mutex.lock();
|
||||
m_thread = std::thread(thread_func, ms, eh, &m_mutex);
|
||||
workers.lock();
|
||||
if (available_workers.empty()) {
|
||||
workers.unlock();
|
||||
s = new state;
|
||||
} else {
|
||||
s = available_workers.back();
|
||||
available_workers.pop_back();
|
||||
workers.unlock();
|
||||
}
|
||||
s->ms = ms;
|
||||
s->eh = eh;
|
||||
s->m_mutex.lock();
|
||||
s->work = 1;
|
||||
if (!s->m_thread) {
|
||||
s->m_thread = new std::thread(thread_func, s);
|
||||
s->m_thread->detach();
|
||||
} else {
|
||||
s->cv.notify_one();
|
||||
}
|
||||
}
|
||||
|
||||
~imp() {
|
||||
m_mutex.unlock();
|
||||
m_thread.join();
|
||||
s->m_mutex.unlock();
|
||||
}
|
||||
};
|
||||
|
||||
|
|
Loading…
Reference in a new issue