mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 18:06:15 +00:00
Code Activity

Fix implementation of scoped_timer under Linux where it was

Browse source 
incorrectly assumed that `pthread_cond_timedwait()` would exit
due to a condition variable being signaled or a timeout occuring.

According to the documentation `pthread_cond_timedwait()` might
spuriously wake so we introduce a new variable `m_signal_sent` (that is
guarded by an existing mutex) that is used as the variable to check that
the thread wake was not spurious.

This is intended to partially fix #839 .
This commit is contained in:
Dan Liew 2016-12-11 23:07:48 +00:00
parent 2307a7ffa7
commit bd1f07f864
1 changed files with 16 additions and 3 deletions
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; pthread_cond_t m_cond;
unsigned m_ms; unsigned m_ms;
bool m_initialized; bool m_initialized;
bool m_signal_sent;
#else #else
// Other // Other
#endif #endif
@ -119,10 +120,18 @@ struct scoped_timer::imp {
pthread_mutex_lock(&st->m_mutex); pthread_mutex_lock(&st->m_mutex);
st->m_initialized = true; st->m_initialized = true;
int e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time); int e = 0;
ENSURE(e == 0 || e == ETIMEDOUT); // `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); pthread_mutex_unlock(&st->m_mutex);
if (e == ETIMEDOUT) if (e == ETIMEDOUT)
st->m_eh->operator()(); st->m_eh->operator()();
return 0; return 0;
@ -170,6 +179,7 @@ struct scoped_timer::imp {
// Linux & FreeBSD // Linux & FreeBSD
m_ms = ms; m_ms = ms;
m_initialized = false; m_initialized = false;
m_signal_sent = false;
ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0); ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0);
ENSURE(pthread_cond_init(&m_cond, NULL) == 0); ENSURE(pthread_cond_init(&m_cond, NULL) == 0);
ENSURE(pthread_create(&m_thread_id, NULL, &thread_func, this) == 0); ENSURE(pthread_create(&m_thread_id, NULL, &thread_func, this) == 0);
@ -218,7 +228,10 @@ struct scoped_timer::imp {
if (!init) if (!init)
sched_yield(); sched_yield();
} }
pthread_mutex_lock(&m_mutex);
m_signal_sent = true;
pthread_cond_signal(&m_cond); pthread_cond_signal(&m_cond);
pthread_mutex_unlock(&m_mutex);
pthread_join(m_thread_id, NULL); pthread_join(m_thread_id, NULL);
pthread_cond_destroy(&m_cond); pthread_cond_destroy(&m_cond);