mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Fix a race condition in scoped_timer::finalize

Browse source 
scoped_timer::finalize is called from fork. However, it may race with
other threads creating or freeing timer threads.

This patch reworks scoped_timer::finalize so that it runs only once
(there is no need to repeat it). We remove the assignments "num_workers =
0" and "available_workers.clear();" - they were done without any locks,
thus they were subjects to race condition.

The variable num_workers is deleted because it is not needed.

There was another bug in scoped_timer::finalize - if some workers were
busy, the function would spin-wait for them to terminate. This patch
changes it so that busy workers are ignored.

Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
This commit is contained in:
Mikulas Patocka 2025-04-06 19:11:29 +02:00
parent a4e7bf82da
commit 95d90a7be5
1 changed files with 14 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/util/scoped_timer.cpp
View file

@ -48,7 +48,6 @@ struct scoped_timer_state {
static std::vector<scoped_timer_state*> available_workers;
static std::mutex workers;
static atomic<unsigned> num_workers(0);
static void thread_func(scoped_timer_state *s) {
workers.lock();
@ -94,7 +93,6 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {
// start new thead
workers.unlock();
s = new scoped_timer_state;
++num_workers;
init_state(ms, eh);
s->m_thread = std::thread(thread_func, s);
}
@ -122,34 +120,27 @@ scoped_timer::~scoped_timer() {
void scoped_timer::initialize() {
#ifndef _WINDOWS
static bool pthread_atfork_set = false;
if (!pthread_atfork_set) {
static std::atomic<bool> pthread_atfork_set = false;
if (!pthread_atfork_set.exchange(true)) {
pthread_atfork(finalize, nullptr, nullptr);
pthread_atfork_set = true;
}
#endif
}
void scoped_timer::finalize() {
unsigned deleted = 0;
while (deleted < num_workers) {
workers.lock();
for (auto w : available_workers) {
w->work = EXITING;
w->cv.notify_one();
}
decltype(available_workers) cleanup_workers;
std::swap(available_workers, cleanup_workers);
workers.unlock();
for (auto w : cleanup_workers) {
++deleted;
w->m_thread.join();
delete w;
}
workers.lock();
for (auto w : available_workers) {
w->work = EXITING;
w->cv.notify_one();
}
decltype(available_workers) cleanup_workers;
std::swap(available_workers, cleanup_workers);
workers.unlock();
for (auto w : cleanup_workers) {
w->m_thread.join();
delete w;
}
num_workers = 0;
available_workers.clear();
}
void scoped_timer::init_state(unsigned ms, event_handler * eh) {