Remove lots of dead code

diff --git a/execution.cc b/execution.cc
index 606b9642ebb6ba39bc50581df6c86f6d70bd61af..f601145a69ad3b96c5d487962089e406f09c07e5 100644 (file)
--- 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<bug_message *> 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<ModelAction *> *
 
        // 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<const ModelAction *> * priorset, bool * canprune, bool check_only)
+                                                                                                                                                                       SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
 {
        SnapVector<action_list_t> *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 3a538e13f238cb41249af2587a82752efc41e07c..5e1b18700c248736d7657f04c625eaea1c18b277 100644 (file)
--- 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 cffaea874740ada79a5ee89e0901e31e9dbcdb2c..adfa971a3dd35c6fad556b1d0e09a49fe9338eae 100644 (file)
--- 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 a3a7bc0ee8f22a059a1b9572d82a2f266f9e2a04..b974419fe851e3042088ee94a322d99201e1cd46 100644 (file)
--- a/model.h
+++ b/model.h
@@ -22,10 +22,8 @@ typedef SnapList<ModelAction *> 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 */