prune mod order

diff --git a/execution.cc b/execution.cc
index 8b718ba5fde29ddc6085850934925ff368adb968..f17ed53ca76fa83d504ba711e79ed576505a6b42 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -270,14 +270,18 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelActio
 
 
                ASSERT(rf);
-
-               if (r_modification_order(curr, rf, priorset)) {
+               bool canprune = false;
+               if (r_modification_order(curr, rf, priorset, &canprune)) {
                        for(unsigned int i=0;i<priorset->size();i++) {
                                mo_graph->addEdge((*priorset)[i], rf);
                        }
                        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();
+                       }
                        return;
                }
                priorset->clear();
@@ -764,7 +768,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  * @return True if modification order edges were added; false otherwise
  */
 
-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset)
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;
@@ -847,6 +851,11 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                                if (mo_graph->checkReachable(rf, prevrf))
                                                        return false;
                                                priorset->push_back(prevrf);
+                                       } else {
+                                               if (act->get_tid() == curr->get_tid()) {
+                                                       //Can prune curr from obj list
+                                                       *canprune = true;
+                                               }
                                        }
                                }
                                break;

diff --git a/execution.h b/execution.h
index 990a7a8ab694b9e81559ee582e52ab7e1d592e25..20bbfdc67f6466fe1ba47b46af00e1b6ad84d31e 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -143,7 +143,7 @@ private:
        SnapVector<const ModelAction *> * build_may_read_from(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
 
-       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset);
+       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset, bool *canprune);
        void w_modification_order(ModelAction *curr);
        void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
        bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;