mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 11:52:05 +00:00
Code Activity

scoped_timer: skip extra unneded heap allocation

Browse source
This commit is contained in:
Nuno Lopes 2021-03-01 14:36:22 +00:00
parent fc558d3946
commit db04ccb137
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/util/scoped_timer.cpp
View file

@ -34,7 +34,7 @@ Revision History:
#endif #endif
struct scoped_timer_state { struct scoped_timer_state {
std::thread * m_thread { nullptr }; std::thread m_thread;
std::timed_mutex m_mutex; std::timed_mutex m_mutex;
event_handler * eh; event_handler * eh;
unsigned ms; unsigned ms;
@ -82,9 +82,11 @@ private:
public: public:
imp(unsigned ms, event_handler * eh) { imp(unsigned ms, event_handler * eh) {
workers.lock(); workers.lock();
bool new_worker = false;
if (available_workers.empty()) { if (available_workers.empty()) {
workers.unlock(); workers.unlock();
s = new scoped_timer_state; s = new scoped_timer_state;
new_worker = true;
++num_workers; ++num_workers;
} }
else { else {
@ -96,8 +98,8 @@ public:
s->eh = eh; s->eh = eh;
s->m_mutex.lock(); s->m_mutex.lock();
s->work = 1; s->work = 1;
if (!s->m_thread) { if (new_worker) {
s->m_thread = new std::thread(thread_func, s); s->m_thread = std::thread(thread_func, s);
} }
else { else {
s->cv.notify_one(); s->cv.notify_one();
@ -146,8 +148,7 @@ void scoped_timer::finalize() {
for (auto w : cleanup_workers) { for (auto w : cleanup_workers) {
++deleted; ++deleted;
w->m_thread->join(); w->m_thread.join();
delete w->m_thread;
delete w; delete w;
} }
} }