mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

Fix scoped_timer for Linux. Nested timers were misbehaving, and it was not possible to create timers in more than one thread

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-17 20:46:04 -08:00
parent 607fab486c
commit 9674f511b3
1 changed files with 7 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/util/scoped_timer.cpp
View file

@ -73,9 +73,6 @@ struct scoped_timer::imp {
pthread_cond_t m_condition_var; pthread_cond_t m_condition_var;
#elif defined(_LINUX_) || defined(_FREEBSD_) #elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD // Linux & FreeBSD
static void * g_timer;
void (*m_old_handler)(int);
void * m_old_timer;
timer_t m_timerid; timer_t m_timerid;
#else #else
// Other // Other
@ -128,8 +125,9 @@ struct scoped_timer::imp {
return st; return st;
} }
#elif defined(_LINUX_) || defined(_FREEBSD_) #elif defined(_LINUX_) || defined(_FREEBSD_)
static void sig_handler(int) { static void sig_handler(union sigval s) {
static_cast<imp*>(g_timer)->m_eh->operator()(); void * ptr = s.sival_ptr;
static_cast<imp*>(ptr)->m_eh->operator()();
} }
#else #else
// Other // Other
@ -156,23 +154,11 @@ struct scoped_timer::imp {
throw default_exception("failed to start timer thread"); throw default_exception("failed to start timer thread");
#elif defined(_LINUX_) || defined(_FREEBSD_) #elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD // Linux & FreeBSD
if (omp_in_parallel()) {
// It doesn't work in with more than one thread.
// SIGEV_SIGNAL: the event is handled by the process not by the thread that installed the handler.
// SIGEV_THREAD: the event is handled by a new thread (Z3 crashes with this configuration).
//
// It seems the way to go is SIGEV_SIGNAL, but I have to find a way to identify the thread the event is meant to.
return;
}
m_old_timer = g_timer;
g_timer = this;
m_old_handler = signal(SIG, sig_handler);
struct sigevent sev; struct sigevent sev;
memset(&sev, 0, sizeof(sigevent)); memset(&sev, 0, sizeof(sigevent));
sev.sigev_notify = SIGEV_SIGNAL; sev.sigev_notify = SIGEV_THREAD;
sev.sigev_signo = SIG; sev.sigev_value.sival_ptr = this;
sev.sigev_value.sival_ptr = &m_timerid; sev.sigev_notify_function = sig_handler;
if (timer_create(CLOCKID, &sev, &m_timerid) == -1) if (timer_create(CLOCKID, &sev, &m_timerid) == -1)
throw default_exception("failed to create timer"); throw default_exception("failed to create timer");
@ -182,6 +168,7 @@ struct scoped_timer::imp {
its.it_value.tv_nsec = nano % 1000000000ull; its.it_value.tv_nsec = nano % 1000000000ull;
its.it_interval.tv_sec = 0; // timer experies once its.it_interval.tv_sec = 0; // timer experies once
its.it_interval.tv_nsec = 0; its.it_interval.tv_nsec = 0;
if (timer_settime(m_timerid, 0, &its, NULL) == -1) if (timer_settime(m_timerid, 0, &its, NULL) == -1)
throw default_exception("failed to set timer"); throw default_exception("failed to set timer");
#else #else
@ -203,12 +190,7 @@ struct scoped_timer::imp {
throw default_exception("failed to destroy pthread attributes object"); throw default_exception("failed to destroy pthread attributes object");
#elif defined(_LINUX_) || defined(_FREEBSD_) #elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD // Linux & FreeBSD
if (omp_in_parallel())
return; // see comments in the constructor.
timer_delete(m_timerid); timer_delete(m_timerid);
if (m_old_handler != SIG_ERR)
signal(SIG, m_old_handler);
g_timer = m_old_timer;
#else #else
// Other Platforms // Other Platforms
#endif #endif
@ -216,16 +198,6 @@ struct scoped_timer::imp {
}; };
#if defined(_WINDOWS) || defined(_CYGWIN)
#elif defined(__APPLE__) && defined(__MACH__)
// Mac OS X
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
void * scoped_timer::imp::g_timer = 0;
#else
// Other platforms
#endif
scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {
if (ms != UINT_MAX) if (ms != UINT_MAX)
m_imp = alloc(imp, ms, eh); m_imp = alloc(imp, ms, eh);