More code towards support non-atomic stores

diff --git a/cmodelint.cc b/cmodelint.cc
index 5b37e867d635d4f457c2bbb3dd0212c1d1e58193..9faae5345e857caa7918b278527ba713c9259ef8 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -114,7 +114,7 @@ CDSATOMICINT(64)
 #define CDSATOMICLOAD(size)                                             \
        uint ## size ## _t cds_atomic_load ## size(void * obj, int atomic_index, const char * position) { \
                ensureModel();                                                      \
-               return (uint ## size ## _t) model->switch_to_master( \
+               return (uint ## size ## _t)model->switch_to_master( \
                        new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)); \
        }
 

diff --git a/datarace.cc b/datarace.cc
index af97a20cd91d7caf965073894081aa554ca67299..58c52dd63c7a80baf27f3017cc4c195054a8f524 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -68,6 +68,8 @@ bool hasNonAtomicStore(const void *address) {
                //Do we have a non atomic write with a non-zero clock
                return ((WRITEVECTOR(shadowval) != 0) && !(ATOMICMASK & shadowval));
        } else {
+               if (shadowval == 0)
+                       return false;
                struct RaceRecord *record = (struct RaceRecord *)shadowval;
                return !record->isAtomic && record->writeClock != 0;
        }
@@ -79,6 +81,8 @@ void setAtomicStoreFlag(const void *address) {
        if (ISSHORTRECORD(shadowval)) {
                *shadow = shadowval | ATOMICMASK;
        } else {
+               if (shadowval == 0)
+                       return;
                struct RaceRecord *record = (struct RaceRecord *)shadowval;
                record->isAtomic = 1;
        }

diff --git a/execution.cc b/execution.cc
index b5f86ff006016b1cfa90dc0436c7975a2754afc6..3f8a78cf0dbf6f1643e0f896852d668d992a1b07 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()
@@ -1132,7 +1132,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 void insertIntoActionList(action_list_t *list, ModelAction *act) {
        action_list_t::reverse_iterator rit = list->rbegin();
        modelclock_t next_seq = act->get_seq_number();
-       if ((*rit)->get_seq_number() == next_seq)
+       if (rit == list->rend() || (*rit)->get_seq_number() == next_seq)
                list->push_back(act);
        else {
                for(;rit != list->rend();rit++) {
@@ -1147,6 +1147,28 @@ void insertIntoActionList(action_list_t *list, ModelAction *act) {
        }
 }
 
+void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+       action_list_t::reverse_iterator rit = list->rbegin();
+       modelclock_t next_seq = act->get_seq_number();
+       if (rit == list->rend()) {
+               act->create_cv(NULL);
+       } else if ((*rit)->get_seq_number() == next_seq) {
+               act->create_cv((*rit));
+               list->push_back(act);
+       } else {
+               for(;rit != list->rend();rit++) {
+                       if ((*rit)->get_seq_number() == next_seq) {
+                               act->create_cv((*rit));
+                               action_list_t::iterator it = rit.base();
+                               it++;   //get to right sequence number
+                               it++;   //get to item after it
+                               list->insert(it, act);
+                               break;
+                       }
+               }
+       }
+}
+
 /**
  * Performs various bookkeeping operations for a normal write.  The
  * complication is that we are typically inserting a normal write
@@ -1160,7 +1182,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
        insertIntoActionList(list, act);
-       insertIntoActionList(&action_trace, act);
+       insertIntoActionListAndSetCV(&action_trace, act);
 
        // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());

diff --git a/hashset.h b/hashset.h
index 140b85fb0d27943adfe3ea3bc7f08ed704c28382..7f7febc657cfb36f5de99808b2938274bab73eb9 100644 (file)
--- a/hashset.h
+++ b/hashset.h
@@ -78,7 +78,7 @@ private:
        HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * set;
 };
 
-template<typename _Key, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = snapshot_malloc, void * (* _calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
+template<typename _Key, typename _KeyInt, int _Shift = 0, void * (*_malloc)(size_t) = snapshot_malloc, void * (*_calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
 class HashSet {
 public:
        HashSet(unsigned int initialcapacity = 16, double factor = 0.5) :

diff --git a/hashtable.h b/hashtable.h
index f71203887a6c871fbae10c272d4915b488680f38..c9da5aad4341883bba7225f3bc97f1f2bd04fc9f 100644 (file)
--- a/hashtable.h
+++ b/hashtable.h
@@ -62,7 +62,7 @@ inline bool default_equals(_Key key1, _Key key2) {
  * @tparam _free   Provide your own 'free' for the table, or default to
  *                 snapshotting.
  */
-template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = snapshot_malloc, void * (* _calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, void * (*_malloc)(size_t) = snapshot_malloc, void * (*_calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
 class HashTable {
 public:
        /**

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/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 6214e9bcfcea73f4668351197820473e0ae0d923..4eafe4fbb321415169bf098d95ba44621de21851 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -160,7 +160,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();
 }
 
 /**
@@ -171,15 +171,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
@@ -260,15 +260,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());
 }
 
 /**