From 9674f511b3c1a7fe68a7888e16d298fb0748f5e4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Dec 2012 20:46:04 -0800
Subject: [PATCH] Fix scoped_timer for Linux. Nested timers were misbehaving,
and it was not possible to create timers in more than one thread
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/util/scoped_timer.cpp | 42 +++++++--------------------------------
1 file changed, 7 insertions(+), 35 deletions(-)
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index d475e5489..d0a79cec6 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -73,9 +73,6 @@ struct scoped_timer::imp {
pthread_cond_t m_condition_var;
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
- static void * g_timer;
- void (*m_old_handler)(int);
- void * m_old_timer;
timer_t m_timerid;
#else
// Other
@@ -128,8 +125,9 @@ struct scoped_timer::imp {
return st;
}
#elif defined(_LINUX_) || defined(_FREEBSD_)
- static void sig_handler(int) {
- static_cast<imp*>(g_timer)->m_eh->operator()();
+ static void sig_handler(union sigval s) {
+ void * ptr = s.sival_ptr;
+ static_cast<imp*>(ptr)->m_eh->operator()();
}
#else
// Other
@@ -156,23 +154,11 @@ struct scoped_timer::imp {
throw default_exception("failed to start timer thread");
#elif defined(_LINUX_) || defined(_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;
memset(&sev, 0, sizeof(sigevent));
- sev.sigev_notify = SIGEV_SIGNAL;
- sev.sigev_signo = SIG;
- sev.sigev_value.sival_ptr = &m_timerid;
+ sev.sigev_notify = SIGEV_THREAD;
+ sev.sigev_value.sival_ptr = this;
+ sev.sigev_notify_function = sig_handler;
if (timer_create(CLOCKID, &sev, &m_timerid) == -1)
throw default_exception("failed to create timer");
@@ -182,6 +168,7 @@ struct scoped_timer::imp {
its.it_value.tv_nsec = nano % 1000000000ull;
its.it_interval.tv_sec = 0; // timer experies once
its.it_interval.tv_nsec = 0;
+
if (timer_settime(m_timerid, 0, &its, NULL) == -1)
throw default_exception("failed to set timer");
#else
@@ -203,12 +190,7 @@ struct scoped_timer::imp {
throw default_exception("failed to destroy pthread attributes object");
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
- if (omp_in_parallel())
- return; // see comments in the constructor.
timer_delete(m_timerid);
- if (m_old_handler != SIG_ERR)
- signal(SIG, m_old_handler);
- g_timer = m_old_timer;
#else
// Other Platforms
#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) {
if (ms != UINT_MAX)
m_imp = alloc(imp, ms, eh);