more fixes

diff --git a/execution.cc b/execution.cc
index 32fa727daa9fdd13807b929d2e2fc1abea0e6453..022021cd93c38f018d1bf5eecec63b4cb518e6ac 100644 (file)
--- 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 7f4dcd4cb5ffeb8801f5f68804fb847cd9801a92..02239d5f9f1b5afb5e66313d3c11c607443fef3b 100644 (file)
--- 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 20cddb9cf64da03d7c5742c05bf5a5e0b0734aaa..31c410aa90c663be893ae5504427d7c5b6f5ddde 100644 (file)
--- 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 6bcd6acd349795839af21bea4212b1ba973a6294..0eaffd5eafc66753546035d59c628df44db40d6f 100644 (file)
--- 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<memory_order *>::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 f7c10f86053b9151988524062d0b34b1b5d255c6..5dd5702ebbc824dfaae6453b2fbe7e51aa3d80ca 100644 (file)
--- 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 0234cdaedb1abe17001df485c2099a813e437613..efe1033b0c4dbb5b7d203dc6d53092c996e8d556 100644 (file)
--- 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 057ad9d99a6f7fcc8377a0d7129bf99076a0851c..e2084abf5008e071bb4cd09e55b3d95a71b3a326 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -6,7 +6,6 @@
 #define __THREADS_MODEL_H__
 
 #include <stdint.h>
-
 #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 8b3e0c6191ae7c9333c11fcafff83570819c4863..8d078b51bbfa1a8c0b4bc03b3176afa85f3a4d97 100644 (file)
--- 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);