From cc6b96adbe8bc76d49c71df36de6b9ff99f373dd Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 25 Nov 2019 22:01:01 -0800 Subject: [PATCH] Remove lots of dead code --- execution.cc | 97 +++++++++++++--------------------------------------- execution.h | 4 --- model.cc | 17 +++------ model.h | 2 -- 4 files changed, 27 insertions(+), 93 deletions(-) diff --git a/execution.cc b/execution.cc index 606b9642..f601145a 100644 --- a/execution.cc +++ b/execution.cc @@ -28,7 +28,6 @@ struct model_snapshot_members { next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), bugs(), - bad_synchronization(false), asserted(false) { } @@ -42,7 +41,6 @@ struct model_snapshot_members { modelclock_t used_sequence_numbers; SnapVector bugs; /** @brief Incorrectly-ordered synchronization was made */ - bool bad_synchronization; bool asserted; SNAPSHOTALLOC @@ -185,21 +183,10 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr) } } -/** @brief Alert the model-checker that an incorrectly-ordered - * synchronization was made */ -void ModelExecution::set_bad_synchronization() -{ - priv->bad_synchronization = true; -} - bool ModelExecution::assert_bug(const char *msg) { priv->bugs.push_back(new bug_message(msg)); - if (isfeasibleprefix()) { - set_assert(); - return true; - } return false; } @@ -303,17 +290,17 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * // Remove writes that violate read modification order /* - for (uint i = 0; i < rf_set->size(); i++) { - ModelAction * rf = (*rf_set)[i]; - if (!r_modification_order(curr, rf, NULL, NULL, true)) { - (*rf_set)[i] = rf_set->back(); - rf_set->pop_back(); - } - }*/ + for (uint i = 0; i < rf_set->size(); i++) { + ModelAction * rf = (*rf_set)[i]; + if (!r_modification_order(curr, rf, NULL, NULL, true)) { + (*rf_set)[i] = rf_set->back(); + rf_set->pop_back(); + } + }*/ while(true) { int index = fuzzer->selectWrite(curr, rf_set); - if (index == -1) // no feasible write exists + if (index == -1)// no feasible write exists return false; ModelAction *rf = (*rf_set)[index]; @@ -664,7 +651,7 @@ void ModelExecution::read_from(ModelAction *act, ModelAction *rf) bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second) { if (*second < *first) { - set_bad_synchronization(); + ASSERT(0); //This should not happend return false; } return second->synchronize_with(first); @@ -735,10 +722,10 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) delete rf_set; /* bool success = process_read(curr, rf_set); - delete rf_set; - if (!success) - return curr; // Do not add action to lists -*/ + delete rf_set; + if (!success) + return curr; // Do not add action to lists + */ } else ASSERT(rf_set == NULL); @@ -763,42 +750,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) return curr; } -/** - * This is the strongest feasibility check available. - * @return whether the current trace (partial or complete) must be a prefix of - * a feasible trace. - */ -bool ModelExecution::isfeasibleprefix() const -{ - return !is_infeasible(); -} - -/** - * Print disagnostic information about an infeasible execution - * @param prefix A string to prefix the output with; if NULL, then a default - * message prefix will be provided - */ -void ModelExecution::print_infeasibility(const char *prefix) const -{ - char buf[100]; - char *ptr = buf; - if (priv->bad_synchronization) - ptr += sprintf(ptr, "[bad sw ordering]"); - if (ptr != buf) - model_print("%s: %s", prefix ? prefix : "Infeasible", buf); -} - -/** - * Check if the current partial trace is infeasible. Does not check any - * end-of-execution flags, which might rule out the execution. Thus, this is - * useful only for ruling an execution as infeasible. - * @return whether the current partial trace is infeasible. - */ -bool ModelExecution::is_infeasible() const -{ - return priv->bad_synchronization; -} - /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ ModelAction * ModelExecution::process_rmw(ModelAction *act) { ModelAction *lastread = get_last_action(act->get_tid()); @@ -830,7 +781,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { */ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, - SnapVector * priorset, bool * canprune, bool check_only) + SnapVector * priorset, bool * canprune, bool check_only) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -1170,7 +1121,7 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act) if ((int)vec->size() <= uninit_id) { int oldsize = (int) vec->size(); vec->resize(uninit_id + 1); - for(int i = oldsize; i < uninit_id + 1; i++) { + for(int i = oldsize;i < uninit_id + 1;i++) { new (&(*vec)[i]) action_list_t(); } } @@ -1186,7 +1137,7 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act) if ((int)vec->size() <= tid) { uint oldsize = vec->size(); vec->resize(priv->next_thread_id); - for(uint i = oldsize; i < priv->next_thread_id; i++) + for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } if (uninit) @@ -1221,7 +1172,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act) if ((int)vec->size() <= tid) { uint oldsize = vec->size(); vec->resize(priv->next_thread_id); - for(uint i = oldsize; i < priv->next_thread_id; i++) + for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } (*vec)[tid].push_back(act); @@ -1246,7 +1197,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act) if ((int)vec->size() <= tid) { uint oldsize = vec->size(); vec->resize(priv->next_thread_id); - for(uint i = oldsize; i < priv->next_thread_id; i++) + for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } (*vec)[tid].push_back(act); @@ -1619,13 +1570,11 @@ void ModelExecution::print_summary() #endif model_print("Execution trace %d:", get_execution_number()); - if (isfeasibleprefix()) { - if (scheduler->all_threads_sleeping()) - model_print(" SLEEP-SET REDUNDANT"); - if (have_bug_reports()) - model_print(" DETECTED BUG(S)"); - } else - print_infeasibility(" INFEASIBLE"); + if (scheduler->all_threads_sleeping()) + model_print(" SLEEP-SET REDUNDANT"); + if (have_bug_reports()) + model_print(" DETECTED BUG(S)"); + model_print("\n"); print_list(&action_trace); diff --git a/execution.h b/execution.h index 3a538e13..5e1b1870 100644 --- a/execution.h +++ b/execution.h @@ -61,7 +61,6 @@ public: ClockVector * get_cv(thread_id_t tid) const; ModelAction * get_parent_action(thread_id_t tid) const; - bool isfeasibleprefix() const; ModelAction * get_last_action(thread_id_t tid) const; @@ -77,8 +76,6 @@ public: void set_assert(); bool is_complete_execution() const; - void print_infeasibility(const char *prefix) const; - bool is_infeasible() const; bool is_deadlocked() const; action_list_t * get_action_trace() { return &action_trace; } @@ -108,7 +105,6 @@ private: Scheduler * const scheduler; bool mo_may_allow(const ModelAction *writer, const ModelAction *reader); - void set_bad_synchronization(); bool should_wake_up(const ModelAction *curr, const Thread *thread) const; void wake_up_sleeping_actions(ModelAction *curr); modelclock_t get_next_seq_num(); diff --git a/model.cc b/model.cc index cffaea87..adfa971a 100644 --- a/model.cc +++ b/model.cc @@ -175,15 +175,12 @@ void ModelChecker::print_bugs() const void ModelChecker::record_stats() { stats.num_total ++; - if (!execution->isfeasibleprefix()) - stats.num_infeasible ++; - else if (execution->have_bug_reports()) + if (execution->have_bug_reports()) stats.num_buggy_executions ++; else if (execution->is_complete_execution()) stats.num_complete ++; else { - stats.num_redundant ++; - + //All threads are sleeping /** * @todo We can violate this ASSERT() when fairness/sleep sets * conflict to cause an execution to terminate, e.g. with: @@ -197,9 +194,7 @@ void ModelChecker::record_stats() void ModelChecker::print_stats() const { model_print("Number of complete, bug-free executions: %d\n", stats.num_complete); - model_print("Number of redundant executions: %d\n", stats.num_redundant); model_print("Number of buggy executions: %d\n", stats.num_buggy_executions); - model_print("Number of infeasible executions: %d\n", stats.num_infeasible); model_print("Total executions: %d\n", stats.num_total); } @@ -238,8 +233,7 @@ bool ModelChecker::next_execution() { DBG(); /* Is this execution a feasible execution that's worth bug-checking? */ - bool complete = execution->isfeasibleprefix() && - (execution->is_complete_execution() || + bool complete = (execution->is_complete_execution() || execution->have_bug_reports()); /* End-of-execution bug checks */ @@ -360,10 +354,7 @@ void ModelChecker::startChecker() { bool ModelChecker::should_terminate_execution() { - /* Infeasible -> don't take any more steps */ - if (execution->is_infeasible()) - return true; - else if (execution->isfeasibleprefix() && execution->have_bug_reports()) { + if (execution->have_bug_reports()) { execution->set_assert(); return true; } else if (execution->isFinished()) { diff --git a/model.h b/model.h index a3a7bc0e..b974419f 100644 --- a/model.h +++ b/model.h @@ -22,10 +22,8 @@ typedef SnapList action_list_t; /** @brief Model checker execution stats */ struct execution_stats { int num_total; /**< @brief Total number of executions */ - int num_infeasible; /**< @brief Number of infeasible executions */ int num_buggy_executions; /** @brief Number of buggy executions */ int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */ - int num_redundant; /**< @brief Number of redundant, aborted executions */ }; /** @brief The central structure for model-checking */ -- 2.34.1