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

Merge pull request #841 from delcypher/scope_timer_spurious_wakes

Browse source 
Make `scoped_timer` robust to spurious wakes under Linux.
This commit is contained in:
Nikolaj Bjorner 2016-12-19 08:22:03 -08:00 committed by GitHub
parent 08f95bedf7 bd1f07f864
commit 0c6c104f9a
1 changed files with 16 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/util/scoped_timer.cpp
View file

@ -73,6 +73,7 @@ struct scoped_timer::imp {
pthread_cond_t m_cond;
unsigned m_ms;
bool m_initialized;
bool m_signal_sent;
#else
// Other
#endif
@ -119,10 +120,18 @@ struct scoped_timer::imp {
pthread_mutex_lock(&st->m_mutex);
st->m_initialized = true;
int e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time);
ENSURE(e == 0 || e == ETIMEDOUT);
int e = 0;
// `pthread_cond_timedwait()` may spuriously wake even if the signal
// was not sent so we loop until a timeout occurs or the signal was
// **really** sent.
while (!(e == 0 && st->m_signal_sent)) {
e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time);
ENSURE(e == 0 || e == ETIMEDOUT);
if (e == ETIMEDOUT)
break;
}
pthread_mutex_unlock(&st->m_mutex);
if (e == ETIMEDOUT)
st->m_eh->operator()();
return 0;
@ -170,6 +179,7 @@ struct scoped_timer::imp {
// Linux & FreeBSD
m_ms = ms;
m_initialized = false;
m_signal_sent = false;
ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0);
ENSURE(pthread_cond_init(&m_cond, NULL) == 0);
ENSURE(pthread_create(&m_thread_id, NULL, &thread_func, this) == 0);
@ -218,7 +228,10 @@ struct scoped_timer::imp {
if (!init)
sched_yield();
}
pthread_mutex_lock(&m_mutex);
m_signal_sent = true;
pthread_cond_signal(&m_cond);
pthread_mutex_unlock(&m_mutex);
pthread_join(m_thread_id, NULL);
pthread_cond_destroy(&m_cond);