From 3c4cdc788494bfd2fa3b22e6487c465132b59006 Mon Sep 17 00:00:00 2001 From: root Date: Mon, 22 Jul 2019 16:40:32 -0700 Subject: [PATCH] remove some datarace code --- cmodelint.cc | 16 ++++++++-------- execution.cc | 33 ++++++--------------------------- execution.h | 1 - funcnode.cc | 6 +++--- history.cc | 4 ++-- model.cc | 22 ---------------------- model.h | 1 - 7 files changed, 19 insertions(+), 64 deletions(-) diff --git a/cmodelint.cc b/cmodelint.cc index d3b64b15..92eea851 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -95,10 +95,10 @@ void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) // cds volatile loads #define VOLATILELOAD(size) \ - uint ## size ## _t cds_volatile_load ## size(void * obj, const char * position) { \ - ensureModel(); \ - return (uint ## size ## _t) model->switch_to_master(new ModelAction(ATOMIC_READ, position, memory_order_relaxed, obj)); \ - } + uint ## size ## _t cds_volatile_load ## size(void * obj, const char * position) { \ + ensureModel(); \ + return (uint ## size ## _t)model->switch_to_master(new ModelAction(ATOMIC_READ, position, memory_order_relaxed, obj)); \ + } VOLATILELOAD(8) VOLATILELOAD(16) @@ -107,10 +107,10 @@ VOLATILELOAD(64) // cds volatile stores #define VOLATILESTORE(size) \ - void cds_volatile_store ## size (void * obj, uint ## size ## _t val, const char * position) { \ - ensureModel(); \ - model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, memory_order_relaxed, obj, (uint64_t) val)); \ -} + void cds_volatile_store ## size (void * obj, uint ## size ## _t val, const char * position) { \ + ensureModel(); \ + model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, memory_order_relaxed, obj, (uint64_t) val)); \ + } VOLATILESTORE(8) VOLATILESTORE(16) diff --git a/execution.cc b/execution.cc index 323c83d3..33a608d6 100644 --- a/execution.cc +++ b/execution.cc @@ -27,7 +27,6 @@ struct model_snapshot_members { next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), bugs(), - dataraces(), bad_synchronization(false), asserted(false) { } @@ -35,16 +34,12 @@ struct model_snapshot_members { ~model_snapshot_members() { for (unsigned int i = 0;i < bugs.size();i++) delete bugs[i]; - for (unsigned int i = 0;i < dataraces.size(); i++) - delete dataraces[i]; bugs.clear(); - dataraces.clear(); } unsigned int next_thread_id; modelclock_t used_sequence_numbers; SnapVector bugs; - SnapVector dataraces; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; bool asserted; @@ -190,22 +185,6 @@ bool ModelExecution::assert_bug(const char *msg) return false; } -/* @brief Put data races in a different list from other bugs. The purpose - * is to continue the program untill the number of data races exceeds a - * threshold */ - -/* TODO: check whether set_assert should be called */ -bool ModelExecution::assert_race(const char *msg) -{ - priv->dataraces.push_back(new bug_message(msg)); - - if (isfeasibleprefix()) { - set_assert(); - return true; - } - return false; -} - /** @return True, if any bugs have been reported for this execution */ bool ModelExecution::have_bug_reports() const { @@ -213,13 +192,13 @@ bool ModelExecution::have_bug_reports() const } /** @return True, if any fatal bugs have been reported for this execution. - * Any bug other than a data race is considered a fatal bug. Data races + * Any bug other than a data race is considered a fatal bug. Data races * are not considered fatal unless the number of races is exceeds - * a threshold (temporarily set as 15). + * a threshold (temporarily set as 15). */ bool ModelExecution::have_fatal_bug_reports() const { - return priv->bugs.size() != 0 || priv->dataraces.size() >= 15; + return priv->bugs.size() != 0; } SnapVector * ModelExecution::get_bugs() const @@ -310,8 +289,8 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector * SnapVector * priorset = new SnapVector(); bool hasnonatomicstore = hasNonAtomicStore(curr->get_location()); if (hasnonatomicstore) { - ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location()); - rf_set->push_back(nonatomicstore); + ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location()); + rf_set->push_back(nonatomicstore); } while(true) { @@ -1209,7 +1188,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); insertIntoActionListAndSetCV(&action_trace, act); - + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); insertIntoActionList(list, act); diff --git a/execution.h b/execution.h index 74496c67..f1d3dc56 100644 --- a/execution.h +++ b/execution.h @@ -68,7 +68,6 @@ public: bool check_action_enabled(ModelAction *curr); bool assert_bug(const char *msg); - bool assert_race(const char *msg); bool have_bug_reports() const; bool have_fatal_bug_reports() const; diff --git a/funcnode.cc b/funcnode.cc index e07ab9e2..27a9abd7 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -40,7 +40,7 @@ FuncInst * FuncNode::get_or_add_action(ModelAction *act) func_inst = new FuncInst(act, this); inst->get_collisions()->push_back(func_inst); - inst_list.push_back(func_inst); // delete? + inst_list.push_back(func_inst); // delete? return func_inst; } @@ -126,7 +126,7 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid) /* Store the memory locations where atomic reads happen */ bool push_loc = true; ModelList::iterator it; - for (it = read_locations.begin(); it != read_locations.end(); it++) { + for (it = read_locations.begin();it != read_locations.end();it++) { if (location == *it) { push_loc = false; break; @@ -172,7 +172,7 @@ void FuncNode::print_last_read(uint32_t tid) read_map_t * read_map = thrd_read_map[tid]; ModelList::iterator it; - for (it = read_locations.begin(); it != read_locations.end(); it++) { + for (it = read_locations.begin();it != read_locations.end();it++) { if ( !read_map->contains(*it) ) break; diff --git a/history.cc b/history.cc index 352a9a4c..6b263ad2 100644 --- a/history.cc +++ b/history.cc @@ -10,7 +10,7 @@ /** @brief Constructor */ ModelHistory::ModelHistory() : - func_counter(1), /* function id starts with 1 */ + func_counter(1), /* function id starts with 1 */ func_map(), func_map_rev(), func_nodes() @@ -136,7 +136,7 @@ FuncNode * ModelHistory::get_func_node(uint32_t func_id) void ModelHistory::print() { /* function id starts with 1 */ - for (uint32_t i = 1; i < func_nodes.size(); i++) { + for (uint32_t i = 1;i < func_nodes.size();i++) { FuncNode * func_node = func_nodes[i]; func_inst_list_mt * entry_insts = func_node->get_entry_insts(); diff --git a/model.cc b/model.cc index cfbc3b86..45fa1b20 100644 --- a/model.cc +++ b/model.cc @@ -139,28 +139,6 @@ bool ModelChecker::assert_bug(const char *msg, ...) return execution->assert_bug(str); } -/** - * @brief Assert a data race in the executing program. - * - * Different from assert_bug, the program will not be aborted immediately - * upon calling this function, unless the number of data races exceeds - * a threshold. - * - * @param msg Descriptive message for the bug (do not include newline char) - * @return True if bug is immediately-feasible - */ -bool ModelChecker::assert_race(const char *msg, ...) -{ - char str[800]; - - va_list ap; - va_start(ap, msg); - vsnprintf(str, sizeof(str), msg, ap); - va_end(ap); - - return execution->assert_race(str); -} - /** * @brief Assert a bug in the executing program, asserted by a user thread * @see ModelChecker::assert_bug diff --git a/model.h b/model.h index a37bd49d..9fb94228 100644 --- a/model.h +++ b/model.h @@ -59,7 +59,6 @@ public: uint64_t switch_to_master(ModelAction *act); bool assert_bug(const char *msg, ...); - bool assert_race(const char *msg, ...); void assert_user_bug(const char *msg); -- 2.34.1