edits

diff --git a/execution.cc b/execution.cc
index de2cace8cecbe61116e74c13837d3dcaedac8c8c..32fa727daa9fdd13807b929d2e2fc1abea0e6453 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -63,10 +63,11 @@ 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()
+       thrd_func_inst_lists(),
+       isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());
@@ -479,10 +480,8 @@ bool ModelExecution::process_fence(ModelAction *curr)
  * @param curr The current action
  * @return True if synchronization was updated or a thread completed
  */
-bool ModelExecution::process_thread_action(ModelAction *curr)
+void ModelExecution::process_thread_action(ModelAction *curr)
 {
-       bool updated = false;
-
        switch (curr->get_type()) {
        case THREAD_CREATE: {
                thrd_t *thrd = (thrd_t *)curr->get_location();
@@ -512,19 +511,25 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);
-               updated = true; /* trigger rel-seq checks */
                break;
        }
        case PTHREAD_JOIN: {
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
                synchronize(act, curr);
-               updated = true; /* trigger rel-seq checks */
                break;  // WL: to be add (modified)
        }
 
+       case THREADONLY_FINISH:
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
+               if (curr == THREAD_FINISH &&
+                               th == model->getInitThread()) {
+                       th->complete();
+                       setFinished();
+                       break;
+               }
+
                /* Wake up any joining threads */
                for (unsigned int i = 0;i < get_num_threads();i++) {
                        Thread *waiting = get_thread(int_to_id(i));
@@ -533,7 +538,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                                scheduler->wake(waiting);
                }
                th->complete();
-               updated = true; /* trigger rel-seq checks */
                break;
        }
        case THREAD_START: {
@@ -542,8 +546,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
        default:
                break;
        }
-
-       return updated;
 }
 
 /**

diff --git a/execution.h b/execution.h
index e958148fc92651c4abe2ce768dc37f9ba61fe912..5a6c40ac1a61d5a5ce8d013987a79b2f908c87aa 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -91,6 +91,8 @@ public:
 
        SnapVector<func_id_list_t> * get_thrd_func_list() { return &thrd_func_list; }
        SnapVector< SnapList<func_inst_list_t *> *> * get_thrd_func_inst_lists() { return &thrd_func_inst_lists; }
+       bool isFinished() {return isfinished;}
+       void setFinished() {isfinished = true;}
 
        SNAPSHOTALLOC
 private:
@@ -116,7 +118,7 @@ private:
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
 
-       bool process_thread_action(ModelAction *curr);
+       void process_thread_action(ModelAction *curr);
        void read_from(ModelAction *act, ModelAction *rf);
        bool synchronize(const ModelAction *first, ModelAction *second);
 
@@ -212,6 +214,7 @@ private:
         * This data structure is handled by ModelHistory
         */
        SnapVector< SnapList< func_inst_list_t *> *> thrd_func_inst_lists;
+       bool isfinished;
 };
 
 #endif /* __EXECUTION_H__ */

diff --git a/funcinst.cc b/funcinst.cc
index 92890d58ce07b296daa0b7bb1c0c17e717d4bb78..2129883944bbed6185964d76f8b6951b2a1711b5 100644 (file)
--- a/funcinst.cc
+++ b/funcinst.cc
@@ -58,11 +58,11 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act)
 
 bool FuncInst::is_read() const
 {
-       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS; /* type == ATOMIC_RMW ? */
+       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS;    /* type == ATOMIC_RMW ? */
 }
 
 bool FuncInst::is_write() const
 {
-        return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE;
+       return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE;
 }
 

diff --git a/funcinst.h b/funcinst.h
index efdb43b4dbe88c9250cb62ecaca8848bbfce1f95..bc56e2772544869097979b42bee45e7f44b1b675 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -48,5 +48,5 @@ private:
        func_inst_list_mt successors;
 };
 
-#endif /* __FUNCINST_H__ */
+#endif /* __FUNCINST_H__ */
 

diff --git a/funcnode.cc b/funcnode.cc
index 208bc3beb2666520d20ac30f873234b1e9775e00..c2a0ea9d17b21defe8b6aeb75dac10739b53cad9 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -117,7 +117,7 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid)
        uint32_t old_size = thrd_read_map.size();
        if (old_size <= tid) {
                thrd_read_map.resize(tid + 1);
-               for (uint32_t i = old_size; i < tid + 1; i++)
+               for (uint32_t i = old_size;i < tid + 1;i++)
                        thrd_read_map[i] = new read_map_t();
        }
 
@@ -167,7 +167,7 @@ void FuncNode::clear_read_map(uint32_t tid)
 
 void FuncNode::generate_predicate(FuncInst *func_inst)
 {
-       
+
 }
 
 /* @param tid thread id

diff --git a/funcnode.h b/funcnode.h
index 08e07fb188ffcbd009f2ee6b160f0b674fd97935..ebd04c7f277986f1355ea91193c0d9c9967339f9 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -56,4 +56,4 @@ private:
        ModelList<void *> read_locations;
 };
 
-#endif /* __FUNCNODE_H__ */
+#endif /* __FUNCNODE_H__ */

diff --git a/history.h b/history.h
index 4457750e961ee69c076ee7b00d91bf98c2f842c3..ee07f993458363041a6c30326d76ef5eb9e0af43 100644 (file)
--- a/history.h
+++ b/history.h
@@ -47,4 +47,4 @@ private:
        HashTable<void *, write_set_t *, uintptr_t, 4, model_malloc, model_calloc, model_free> write_history;
 };
 
-#endif /* __HISTORY_H__ */
+#endif /* __HISTORY_H__ */

diff --git a/include/impatomic.h b/include/impatomic.h
index 02239d5f9f1b5afb5e66313d3c11c607443fef3b..7f4dcd4cb5ffeb8801f5f68804fb847cd9801a92 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/wildcard.h b/include/wildcard.h
index 0eaffd5eafc66753546035d59c628df44db40d6f..6bcd6acd349795839af21bea4212b1ba973a6294 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 65b597defb0b10294083f57a468b6886e7ae17b0..f7c10f86053b9151988524062d0b34b1b5d255c6 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());
 }
 
 /**
@@ -363,6 +363,8 @@ bool ModelChecker::should_terminate_execution()
        else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
                execution->set_assert();
                return true;
+       } else if (execution->isFinished()) {
+               return true;
        }
        return false;
 }

diff --git a/predicate.cc b/predicate.cc
index 9f4246e953a94cde78b88d55dc331016a501222f..c7915006f7d01f96dfa8b355544e3e17cfca5230 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -17,7 +17,7 @@ inline bool operator==(const predicate_expr& expr_A, const predicate_expr& expr_
 void Predicate::add_predicate(predicate_expr predicate)
 {
        ModelList<predicate_expr>::iterator it;
-       for (it = predicates.begin(); it != predicates.end(); it++) {
+       for (it = predicates.begin();it != predicates.end();it++) {
                if (predicate == *it)
                        return;
        }

diff --git a/predicate.h b/predicate.h
index e2412d186705e079e60dabe68762b085af1245b8..bab7a7eee54363c01802bdf44616f0e814bb892e 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -5,7 +5,7 @@ typedef enum predicate_token {
 } token_t;
 
 /* If token is EQUALITY, then the predicate asserts whether
- * this load should read the same value as the last value 
+ * this load should read the same value as the last value
  * read at memory location specified in predicate_expr.
  */
 struct predicate_expr {