From ec7cf0eb61ee239b3da1f184a9e43f77b0dcc25d Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 29 Jul 2019 14:47:55 -0700 Subject: [PATCH] edits --- execution.cc | 22 ++++++++++++---------- execution.h | 5 ++++- funcinst.cc | 4 ++-- funcinst.h | 2 +- funcnode.cc | 4 ++-- funcnode.h | 2 +- history.h | 2 +- include/impatomic.h | 26 +++++++++++++------------- include/wildcard.h | 4 ++-- model.cc | 20 +++++++++++--------- predicate.cc | 2 +- predicate.h | 2 +- 12 files changed, 51 insertions(+), 44 deletions(-) diff --git a/execution.cc b/execution.cc index de2cace8..32fa727d 100644 --- 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 e958148f..5a6c40ac 100644 --- a/execution.h +++ b/execution.h @@ -91,6 +91,8 @@ public: SnapVector * get_thrd_func_list() { return &thrd_func_list; } SnapVector< SnapList *> * 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 92890d58..21298839 100644 --- 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 efdb43b4..bc56e277 100644 --- 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 208bc3be..c2a0ea9d 100644 --- 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 08e07fb1..ebd04c7f 100644 --- a/funcnode.h +++ b/funcnode.h @@ -56,4 +56,4 @@ private: ModelList read_locations; }; -#endif /* __FUNCNODE_H__ */ +#endif /* __FUNCNODE_H__ */ diff --git a/history.h b/history.h index 4457750e..ee07f993 100644 --- a/history.h +++ b/history.h @@ -47,4 +47,4 @@ private: HashTable write_history; }; -#endif /* __HISTORY_H__ */ +#endif /* __HISTORY_H__ */ diff --git a/include/impatomic.h b/include/impatomic.h index 02239d5f..7f4dcd4c 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 0eaffd5e..6bcd6acd 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 65b597de..f7c10f86 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()); } /** @@ -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 9f4246e9..c7915006 100644 --- 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::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 e2412d18..bab7a7ee 100644 --- 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 { -- 2.34.1