From c8b9d01f03c5ceae9b3ad503e29f6900564cc242 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 29 Jul 2019 17:54:01 -0700 Subject: [PATCH] more fixes --- execution.cc | 4 +-- include/impatomic.h | 26 ++++++++-------- include/mypthread.h | 75 --------------------------------------------- include/wildcard.h | 4 +-- model.cc | 18 +++++------ pthread.cc | 2 ++ threads-model.h | 9 +++++- threads.cc | 16 +++++++++- 8 files changed, 51 insertions(+), 103 deletions(-) diff --git a/execution.cc b/execution.cc index 32fa727d..022021cd 100644 --- a/execution.cc +++ b/execution.cc @@ -63,7 +63,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : thrd_last_action(1), thrd_last_fence_release(), priv(new struct model_snapshot_members ()), - mo_graph(new CycleGraph()), + mo_graph(new CycleGraph()), fuzzer(new Fuzzer()), thrd_func_list(), thrd_func_inst_lists(), @@ -523,7 +523,7 @@ void ModelExecution::process_thread_action(ModelAction *curr) case THREADONLY_FINISH: case THREAD_FINISH: { Thread *th = get_thread(curr); - if (curr == THREAD_FINISH && + if (curr->get_type() == THREAD_FINISH && th == model->getInitThread()) { th->complete(); setFinished(); diff --git a/include/impatomic.h b/include/impatomic.h index 7f4dcd4c..02239d5f 100644 --- a/include/impatomic.h +++ b/include/impatomic.h @@ -82,12 +82,12 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile #define _ATOMIC_LOAD_( __a__, __x__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__((__a__)->__f__) __r__ = (__typeof__((__a__)->__f__))model_read_action((void *)__p__, __x__); \ + __typeof__((__a__)->__f__)__r__ = (__typeof__((__a__)->__f__))model_read_action((void *)__p__, __x__); \ __r__; }) #define _ATOMIC_STORE_( __a__, __m__, __x__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__(__m__) __v__ = (__m__); \ + __typeof__(__m__)__v__ = (__m__); \ model_write_action((void *) __p__, __x__, (uint64_t) __v__); \ __v__ = __v__; /* Silence clang (-Wunused-value) */ \ }) @@ -95,16 +95,16 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile #define _ATOMIC_INIT_( __a__, __m__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__(__m__) __v__ = (__m__); \ + __typeof__(__m__)__v__ = (__m__); \ model_init_action((void *) __p__, (uint64_t) __v__); \ __v__ = __v__; /* Silence clang (-Wunused-value) */ \ }) #define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); \ - __typeof__(__m__) __v__ = (__m__); \ - __typeof__((__a__)->__f__) __copy__= __old__; \ + __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); \ + __typeof__(__m__)__v__ = (__m__); \ + __typeof__((__a__)->__f__)__copy__= __old__; \ __copy__ __o__ __v__; \ model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); \ __old__ = __old__; /* Silence clang (-Wunused-value) */ \ @@ -115,10 +115,10 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile #define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ ) \ ({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \ - __typeof__(__e__) __q__ = (__e__); \ - __typeof__(__m__) __v__ = (__m__); \ + __typeof__(__e__)__q__ = (__e__); \ + __typeof__(__m__)__v__ = (__m__); \ bool __r__; \ - __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__))model_rmwrcas_action((void *)__p__, __x__, (uint64_t) *__q__, sizeof((__a__)->__f__)); \ + __typeof__((__a__)->__f__)__t__=(__typeof__((__a__)->__f__))model_rmwrcas_action((void *)__p__, __x__, (uint64_t) *__q__, sizeof((__a__)->__f__)); \ if (__t__ == *__q__ ) {; \ model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \ else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \ @@ -2418,8 +2418,8 @@ inline void* atomic_fetch_add_explicit ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ ) { volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); - __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); - __typeof__((__a__)->__f__) __copy__= __old__; + __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); + __typeof__((__a__)->__f__)__copy__= __old__; __copy__ = (void *) (((char *)__copy__) + __m__); model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); return __old__; @@ -2434,8 +2434,8 @@ inline void* atomic_fetch_sub_explicit ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ ) { volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); - __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); - __typeof__((__a__)->__f__) __copy__= __old__; + __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); + __typeof__((__a__)->__f__)__copy__= __old__; __copy__ = (void *) (((char *)__copy__) - __m__); model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); return __old__; diff --git a/include/mypthread.h b/include/mypthread.h index 20cddb9c..31c410aa 100644 --- a/include/mypthread.h +++ b/include/mypthread.h @@ -17,82 +17,7 @@ struct pthread_params { }; extern "C" { - -pthread_t pthread_self(void); int user_main(int, char**); - -// --- not implemented yet --- - -int pthread_attr_destroy(pthread_attr_t *); -int pthread_attr_getdetachstate(const pthread_attr_t *, int *); -int pthread_attr_getguardsize(const pthread_attr_t *, size_t *); -int pthread_attr_getinheritsched(const pthread_attr_t *, int *); -int pthread_attr_getschedparam(const pthread_attr_t *, - struct sched_param *); -int pthread_attr_getschedpolicy(const pthread_attr_t *, int *); -int pthread_attr_getscope(const pthread_attr_t *, int *); -int pthread_attr_getstackaddr(const pthread_attr_t *, void **); -int pthread_attr_getstacksize(const pthread_attr_t *, size_t *); -int pthread_attr_init(pthread_attr_t *); -int pthread_attr_setdetachstate(pthread_attr_t *, int); -int pthread_attr_setguardsize(pthread_attr_t *, size_t); -int pthread_attr_setinheritsched(pthread_attr_t *, int); -int pthread_attr_setschedparam(pthread_attr_t *, - const struct sched_param *); -int pthread_attr_setschedpolicy(pthread_attr_t *, int); -int pthread_attr_setscope(pthread_attr_t *, int); -int pthread_attr_setstackaddr(pthread_attr_t *, void *); -int pthread_attr_setstacksize(pthread_attr_t *, size_t); -int pthread_cancel(pthread_t); -int pthread_cond_destroy(pthread_cond_t *); -int pthread_condattr_destroy(pthread_condattr_t *); -int pthread_condattr_getpshared(const pthread_condattr_t *, int *); -int pthread_condattr_init(pthread_condattr_t *); -int pthread_condattr_setpshared(pthread_condattr_t *, int); - -int pthread_detach(pthread_t); -int pthread_equal(pthread_t, pthread_t); -int pthread_getconcurrency(void); -int pthread_getschedparam(pthread_t, int *, struct sched_param *); -void *pthread_getspecific(pthread_key_t); -int pthread_key_create(pthread_key_t *, void (*)(void *)); -int pthread_key_delete(pthread_key_t); -int pthread_mutex_destroy(pthread_mutex_t *); -int pthread_mutex_getprioceiling(const pthread_mutex_t *, int *); -int pthread_mutex_setprioceiling(pthread_mutex_t *, int, int *); -int pthread_mutexattr_destroy(pthread_mutexattr_t *); -int pthread_mutexattr_getprioceiling(const pthread_mutexattr_t *, - int *); -int pthread_mutexattr_getprotocol(const pthread_mutexattr_t *, int *); -int pthread_mutexattr_getpshared(const pthread_mutexattr_t *, int *); -int pthread_mutexattr_gettype(const pthread_mutexattr_t *, int *); -int pthread_mutexattr_init(pthread_mutexattr_t *); -int pthread_mutexattr_setprioceiling(pthread_mutexattr_t *, int); -int pthread_mutexattr_setprotocol(pthread_mutexattr_t *, int); -int pthread_mutexattr_setpshared(pthread_mutexattr_t *, int); -int pthread_mutexattr_settype(pthread_mutexattr_t *, int); -int pthread_once(pthread_once_t *, void (*)(void)); -int pthread_rwlock_destroy(pthread_rwlock_t *); -int pthread_rwlock_init(pthread_rwlock_t *, - const pthread_rwlockattr_t *); -int pthread_rwlock_rdlock(pthread_rwlock_t *); -int pthread_rwlock_tryrdlock(pthread_rwlock_t *); -int pthread_rwlock_trywrlock(pthread_rwlock_t *); -int pthread_rwlock_unlock(pthread_rwlock_t *); -int pthread_rwlock_wrlock(pthread_rwlock_t *); -int pthread_rwlockattr_destroy(pthread_rwlockattr_t *); -int pthread_rwlockattr_getpshared(const pthread_rwlockattr_t *, - int *); -int pthread_rwlockattr_init(pthread_rwlockattr_t *); -int pthread_rwlockattr_setpshared(pthread_rwlockattr_t *, int); -int pthread_setcancelstate(int, int *); -int pthread_setcanceltype(int, int *); -int pthread_setconcurrency(int); -int pthread_setschedparam(pthread_t, int, - const struct sched_param *); -int pthread_setspecific(pthread_key_t, const void *); -void pthread_testcancel(void); - } void check(); diff --git a/include/wildcard.h b/include/wildcard.h index 6bcd6acd..0eaffd5e 100644 --- a/include/wildcard.h +++ b/include/wildcard.h @@ -21,11 +21,11 @@ #define is_normal_mo(x) ((x >= memory_order_relaxed && x <= memory_order_seq_cst) || x == memory_order_normal) #define assert_infer(x) for (int i = 0;i <= wildcardNum;i++) \ - ASSERT(is_normal_mo_infer((x[i]))); + ASSERT(is_normal_mo_infer((x[i]))); #define assert_infers(x) for (ModelList::iterator iter = \ (x)->begin();iter != (x)->end();iter++) \ - assert_infer((*iter)); + assert_infer((*iter)); #define relaxed memory_order_relaxed #define release memory_order_release diff --git a/model.cc b/model.cc index f7c10f86..5dd5702e 100644 --- a/model.cc +++ b/model.cc @@ -163,7 +163,7 @@ void ModelChecker::print_bugs() const bugs->size(), bugs->size() > 1 ? "s" : ""); for (unsigned int i = 0;i < bugs->size();i++) - (*bugs)[i]->print(); + (*bugs)[i] -> print(); } /** @@ -174,15 +174,15 @@ void ModelChecker::print_bugs() const */ void ModelChecker::record_stats() { - stats.num_total++; + stats.num_total ++; if (!execution->isfeasibleprefix()) - stats.num_infeasible++; + stats.num_infeasible ++; else if (execution->have_bug_reports()) - stats.num_buggy_executions++; + stats.num_buggy_executions ++; else if (execution->is_complete_execution()) - stats.num_complete++; + stats.num_complete ++; else { - stats.num_redundant++; + stats.num_redundant ++; /** * @todo We can violate this ASSERT() when fairness/sleep sets @@ -262,15 +262,15 @@ bool ModelChecker::next_execution() return true; } // test code - execution_number++; + execution_number ++; reset_to_initial_state(); return false; } /** @brief Run trace analyses on complete trace */ void ModelChecker::run_trace_analyses() { - for (unsigned int i = 0;i < trace_analyses.size();i++) - trace_analyses[i]->analyze(execution->get_action_trace()); + for (unsigned int i = 0;i < trace_analyses.size();i ++) + trace_analyses[i] -> analyze(execution->get_action_trace()); } /** diff --git a/pthread.cc b/pthread.cc index 0234cdae..efe1033b 100644 --- a/pthread.cc +++ b/pthread.cc @@ -57,6 +57,8 @@ void pthread_exit(void *value_ptr) { Thread * th = thread_current(); th->set_pthread_return(value_ptr); model->switch_to_master(new ModelAction(THREADONLY_FINISH, std::memory_order_seq_cst, th)); + //Need to exit so we don't return to the program + real_pthread_exit(NULL); } int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { diff --git a/threads-model.h b/threads-model.h index 057ad9d9..e2084abf 100644 --- a/threads-model.h +++ b/threads-model.h @@ -6,7 +6,6 @@ #define __THREADS_MODEL_H__ #include - #include "mymemory.h" #include "threads.h" #include "modeltypes.h" @@ -211,4 +210,12 @@ static inline int id_to_int(thread_id_t id) return id; } +int real_pthread_mutex_init(pthread_mutex_t *__mutex, const pthread_mutexattr_t *__mutexattr); +int real_pthread_mutex_lock (pthread_mutex_t *__mutex); +int real_pthread_mutex_unlock (pthread_mutex_t *__mutex); +int real_pthread_create (pthread_t *__restrict __newthread, const pthread_attr_t *__restrict __attr, void *(*__start_routine)(void *), void *__restrict __arg); +int real_pthread_join (pthread_t __th, void ** __thread_return); +void real_pthread_exit (void * value_ptr) __attribute__((noreturn)); +void real_init_all(); + #endif /* __THREADS_MODEL_H__ */ diff --git a/threads.cc b/threads.cc index 8b3e0c61..8d078b51 100644 --- a/threads.cc +++ b/threads.cc @@ -92,7 +92,6 @@ void thread_startup() model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread)); } -#ifdef TLS static int (*pthread_mutex_init_p)(pthread_mutex_t *__mutex, const pthread_mutexattr_t *__mutexattr) = NULL; int real_pthread_mutex_init(pthread_mutex_t *__mutex, const pthread_mutexattr_t *__mutexattr) { @@ -123,6 +122,12 @@ int real_pthread_join (pthread_t __th, void ** __thread_return) { return pthread_join_p(__th, __thread_return); } +static void (*pthread_exit_p)(void *) __attribute__((noreturn))= NULL; + +void real_pthread_exit (void * value_ptr) { + pthread_exit_p(value_ptr); +} + void real_init_all() { char * error; if (!pthread_mutex_init_p) { @@ -160,8 +165,17 @@ void real_init_all() { exit(EXIT_FAILURE); } } + + if (!pthread_exit_p) { + pthread_exit_p = (void (*)(void *))dlsym(RTLD_NEXT, "pthread_exit"); + if ((error = dlerror()) != NULL) { + fputs(error, stderr); + exit(EXIT_FAILURE); + } + } } +#ifdef TLS void finalize_helper_thread() { Thread * curr_thread = thread_current(); real_pthread_mutex_lock(&curr_thread->mutex); -- 2.34.1