Fix bug

diff --git a/execution.cc b/execution.cc
index cd277c55daa5ad1471380f6450cd72f51c45977c..9b179880f9cdd81e77762e7b851093ddd79ac167 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -283,7 +283,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
  * Processes a read model action.
  * @param curr is the read model action to process.
  * @param rf_set is the set of model actions we can possibly read from
- * @return True if processing this read updates the mo_graph.
+ * @return True if the read can be pruned from the thread map list.
  */
 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 {
@@ -320,12 +320,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                        read_from(curr, rf);
                        get_thread(curr)->set_return_value(curr->get_return_value());
                        delete priorset;
-                       if (canprune && curr->get_type() == ATOMIC_READ) {
-                               int tid = id_to_int(curr->get_tid());
-                               (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
-                               curr->setThrdMapRef(NULL);
-                       }
-                       return true;
+                       return canprune && curr->get_type() == ATOMIC_READ;
                }
                priorset->clear();
                (*rf_set)[index] = rf_set->back();
@@ -728,15 +723,17 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        if (newly_explored && curr->is_read())
                rf_set = build_may_read_from(curr);
 
+       bool canprune = false;
+
        if (curr->is_read() && !second_part_of_rmw) {
-               process_read(curr, rf_set);
+               canprune = process_read(curr, rf_set);
                delete rf_set;
        } else
                ASSERT(rf_set == NULL);
 
        /* Add the action to lists */
        if (!second_part_of_rmw)
-               add_action_to_lists(curr);
+               add_action_to_lists(curr, canprune);
 
        if (curr->is_write())
                add_write_to_lists(curr);
@@ -1118,7 +1115,7 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
  *
  * @param act is the ModelAction to add.
  */
-void ModelExecution::add_action_to_lists(ModelAction *act)
+void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
 {
        int tid = id_to_int(act->get_tid());
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
@@ -1138,7 +1135,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       act->setThrdMapRef((*vec)[tid].add_back(act));
+       if (!canprune)
+               act->setThrdMapRef((*vec)[tid].add_back(act));
 
        // Update thrd_last_action, the last action taken by each thread
        if ((int)thrd_last_action.size() <= tid)

diff --git a/execution.h b/execution.h
index 2d227d21361a24918a47720139bf8148166d6a01..72efcd6743ae34db51a0a9b75d3f2ce0c08975fc 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -109,7 +109,7 @@ private:
        void process_thread_action(ModelAction *curr);
        void read_from(ModelAction *act, ModelAction *rf);
        bool synchronize(const ModelAction *first, ModelAction *second);
-       void add_action_to_lists(ModelAction *act);
+       void add_action_to_lists(ModelAction *act, bool canprune);
        void add_normal_write_to_lists(ModelAction *act);
        void add_write_to_lists(ModelAction *act);
        ModelAction * get_last_fence_release(thread_id_t tid) const;

diff --git a/model.cc b/model.cc
index 4f8a03243161ec61aa25644159c9856ae01188f8..d1e94e5efa4f70c08486abf646b0ef46a3fae324 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -261,7 +261,7 @@ void ModelChecker::finish_execution(bool more_executions)
 // test code
        execution_number ++;
        if (more_executions)
-         reset_to_initial_state();
+               reset_to_initial_state();
        history->set_new_exec_flag();
 }