mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

Fix issue with bd1f07f864 pointed out by

Browse source 
@nunolopes .

If `pthread_cond_signal()` is called while `m_mutex` is held then the
timing thread might be woken up twice due to waking up from
`pthread_cond_timeout()` (due to being signaled) but then being forced
to sleep again because the thread calling `~imp()` is still holding
`m_mutex` (which the timing thread needs to acquire).
This commit is contained in:
Dan Liew 2016-12-19 22:36:42 +00:00
parent 251d1ec031
commit b5aa6d5eb5
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/util/scoped_timer.cpp
View file

@ -230,8 +230,9 @@ struct scoped_timer::imp {
}
pthread_mutex_lock(&m_mutex);
m_signal_sent = true;
pthread_cond_signal(&m_cond);
pthread_mutex_unlock(&m_mutex);
// Perform signal outside of lock to avoid waking timing thread twice.
pthread_cond_signal(&m_cond);
pthread_join(m_thread_id, NULL);
pthread_cond_destroy(&m_cond);