From c76be793b17d234cc803f89bdda90c89f57ce17e Mon Sep 17 00:00:00 2001 From: root Date: Thu, 18 Jul 2019 19:37:38 -0700 Subject: [PATCH] More code towards support non-atomic stores --- cmodelint.cc | 2 +- datarace.cc | 4 ++++ execution.cc | 28 +++++++++++++++++++++++++--- hashset.h | 2 +- hashtable.h | 2 +- include/impatomic.h | 26 +++++++++++++------------- include/wildcard.h | 4 ++-- model.cc | 18 +++++++++--------- 8 files changed, 56 insertions(+), 30 deletions(-) diff --git a/cmodelint.cc b/cmodelint.cc index 5b37e867..9faae534 100644 --- 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 af97a20c..58c52dd6 100644 --- 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 b5f86ff0..3f8a78cf 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() @@ -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 *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); diff --git a/hashset.h b/hashset.h index 140b85fb..7f7febc6 100644 --- a/hashset.h +++ b/hashset.h @@ -78,7 +78,7 @@ private: HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * set; }; -template, bool (*equals)(_Key, _Key) = default_equals<_Key> > +template, 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 f7120388..c9da5aad 100644 --- 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, bool (*equals)(_Key, _Key) = default_equals<_Key> > +template, bool (*equals)(_Key, _Key) = default_equals<_Key> > class HashTable { public: /** 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/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 6214e9bc..4eafe4fb 100644 --- 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()); } /** -- 2.34.1