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

rewrite scoped_timer for linux

Browse source 
The previous version was racy and could lead to crashes.
The timer could be deleted before the callback was called, making it execute on already freed memory

This new version is similar to Mac's. It spawns its own thread and uses pthread_cond_wait.
Care is taken for small timeouts to avoid races in the thread creation and timer destruction.

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-11-22 11:40:52 +00:00
parent b26735a887
commit d9bafc3fba
2 changed files with 60 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/util/debug.h
View file

@ -19,6 +19,8 @@ Revision History:
#ifndef DEBUG_H_
#define DEBUG_H_
#include <stdlib.h>
void enable_assertions(bool f);
bool assertions_enabled();
@ -82,6 +84,12 @@ bool is_debug_enabled(const char * tag);
#define VERIFY(_x_) (void)(_x_)
#endif
#define ENSURE(_x_) \
if (!(_x_)) { \
std::cerr << "Failed to verify: " << #_x_ << "\n"; \
exit(-1); \
}
#define MAKE_NAME2(LINE) zofty_ ## LINE
#define MAKE_NAME(LINE) MAKE_NAME2(LINE)
#define DBG_UNIQUE_NAME MAKE_NAME(__LINE__)

86
src/util/scoped_timer.cpp
View file

@ -35,17 +35,10 @@ Revision History:
#include<pthread.h>
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux
#include<csignal>
#include<ctime>
#include<memory.h>
#include"warning.h"
#ifdef _LINUX_
#define CLOCKID CLOCK_PROCESS_CPUTIME_ID
#else
// FreeBSD does not support CLOCK_PROCESS_CPUTIME_ID
#define CLOCKID CLOCK_MONOTONIC
#endif
#define SIG SIGRTMIN
#include<errno.h>
#include<pthread.h>
#include<sched.h>
#include<time.h>
// ---------
#else
// Other platforms
@ -75,7 +68,11 @@ struct scoped_timer::imp {
struct timespec m_end_time;
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
timer_t m_timerid;
pthread_t m_thread_id;
pthread_mutex_t m_mutex;
pthread_cond_t m_cond;
unsigned m_ms;
bool m_initialized;
#else
// Other
#endif
@ -107,9 +104,28 @@ struct scoped_timer::imp {
return st;
}
#elif defined(_LINUX_) || defined(_FREEBSD_)
static void sig_handler(union sigval s) {
void * ptr = s.sival_ptr;
static_cast<imp*>(ptr)->m_eh->operator()();
static void* thread_func(void *arg) {
scoped_timer::imp *st = static_cast<scoped_timer::imp*>(arg);
struct timespec end_time;
clock_gettime(CLOCK_REALTIME, &end_time);
end_time.tv_sec += st->m_ms / 1000u;
end_time.tv_nsec += (st->m_ms % 1000u) * 1000000ull;
// check for overflow
if (end_time.tv_nsec >= 1000000000ull) {
++end_time.tv_sec;
end_time.tv_nsec -= 1000000000ull;
}
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);
pthread_mutex_unlock(&st->m_mutex);
if (e == ETIMEDOUT)
st->m_eh->operator()();
return 0;
}
#else
// Other
@ -152,23 +168,11 @@ struct scoped_timer::imp {
throw default_exception("failed to start timer thread");
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
struct sigevent sev;
memset(&sev, 0, sizeof(sigevent));
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");
unsigned long long nano = static_cast<unsigned long long>(ms) * 1000000ull;
struct itimerspec its;
its.it_value.tv_sec = nano / 1000000000ull;
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");
m_ms = ms;
m_initialized = 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);
#else
// Other platforms
#endif
@ -203,8 +207,22 @@ struct scoped_timer::imp {
if (pthread_attr_destroy(&m_attributes) != 0)
throw default_exception("failed to destroy pthread attributes object");
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
timer_delete(m_timerid);
// Linux & FreeBSD
bool init = false;
// spin until timer thread has been created
while (!init) {
pthread_mutex_lock(&m_mutex);
init = m_initialized;
pthread_mutex_unlock(&m_mutex);
if (!init)
sched_yield();
}
pthread_cond_signal(&m_cond);
pthread_join(m_thread_id, NULL);
pthread_cond_destroy(&m_cond);
pthread_mutex_destroy(&m_mutex);
#else
// Other Platforms
#endif