Optimize SC lookup

diff --git a/action.h b/action.h
index 4eb1f7ed19799943b3cf906e4f0a1a2017f1a95d..5862485b7e54b58a70ac10e0800be70f23548c33 100644 (file)
--- a/action.h
+++ b/action.h
@@ -202,7 +202,7 @@ private:
        /** @brief The last fence release from the same thread */
        const ModelAction *last_fence_release;
        ModelAction * uninitaction;
-       
+
        /**
         * @brief The clock vector for this operation
         *
@@ -212,7 +212,7 @@ private:
         */
        ClockVector *cv;
        ClockVector *rf_cv;
-       
+
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;
 

diff --git a/execution.cc b/execution.cc
index de7cfa2ffff23e33961700a77ae40a7a582cb2b8..8877fcdc676c4c807e5f7f94a9e61f3aefb29d4c 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -62,7 +62,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        thrd_last_action(1),
        thrd_last_fence_release(),
        priv(new struct model_snapshot_members ()),
-       mo_graph(new CycleGraph()),
+                        mo_graph(new CycleGraph()),
        fuzzer(new Fuzzer())
 {
        /* Initialize a model-checker thread, for special ModelActions */
@@ -649,6 +649,9 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        if (!second_part_of_rmw && curr->get_type() != NOOP)
                add_action_to_lists(curr);
 
+       if (curr->is_write())
+               add_write_to_lists(curr);
+
        SnapVector<ModelAction *> * rf_set = NULL;
        /* Build may_read_from set for newly-created actions */
        if (newly_explored && curr->is_read())
@@ -1036,9 +1039,9 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
                }
                i--;
                if (i >= 0) {
-                 rf = (*processset)[i];
+                       rf = (*processset)[i];
                } else
-                 break;
+                       break;
        }
        if (processset != NULL)
                delete processset;
@@ -1103,6 +1106,12 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
        }
 }
 
+void ModelExecution::add_write_to_lists(ModelAction *write) {
+       // Update seq_cst map
+       if (write->is_seqcst())
+               obj_last_sc_map.put(write->get_location(), write);
+}
+
 /**
  * @brief Get the last action performed by a particular Thread
  * @param tid The thread ID of the Thread in question
@@ -1142,16 +1151,7 @@ ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
 {
        void *location = curr->get_location();
-       action_list_t *list = obj_map.get(location);
-       /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
-       action_list_t::reverse_iterator rit;
-       for (rit = list->rbegin();(*rit) != curr;rit++)
-               ;
-       rit++;  /* Skip past curr */
-       for ( ;rit != list->rend();rit++)
-               if ((*rit)->is_write() && (*rit)->is_seqcst())
-                       return *rit;
-       return NULL;
+       return obj_last_sc_map.get(location);
 }
 
 /**

diff --git a/execution.h b/execution.h
index 150fc68becc369c7b2f9c605adf0ee912890eeb8..89b3200afba9379c0730b946fd13de6c45c7d3cd 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -115,6 +115,7 @@ private:
        bool synchronize(const ModelAction *first, ModelAction *second);
 
        void add_action_to_lists(ModelAction *act);
+       void add_write_to_lists(ModelAction *act);
        ModelAction * get_last_fence_release(thread_id_t tid) const;
        ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
        ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const;
@@ -144,7 +145,7 @@ private:
 
        HashTable<const void *, ModelAction *, uintptr_t, 4> obj_last_sc_map;
 
-       
+
        HashTable<pthread_mutex_t *, cdsc::snapmutex *, uintptr_t, 4> mutex_map;
        HashTable<pthread_cond_t *, cdsc::snapcondition_variable *, uintptr_t, 4> cond_map;
 

diff --git a/model.cc b/model.cc
index 3b4784d2e1fe2b364038c546542bd179716c2b8f..1791695432cc0e7f3348e1564c06fd58c030d062 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -316,17 +316,17 @@ void ModelChecker::switch_from_master(Thread *thread)
  */
 uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
-  if (forklock) {
-    static bool fork_message_printed = false;
-
-    if (!fork_message_printed) {
-      model_print("Fork handler trying to call into model checker...\n");
-      fork_message_printed = true;
-    }
-    delete act;
-    return 0;
-  }
-  DBG();
+       if (forklock) {
+               static bool fork_message_printed = false;
+
+               if (!fork_message_printed) {
+                       model_print("Fork handler trying to call into model checker...\n");
+                       fork_message_printed = true;
+               }
+               delete act;
+               return 0;
+       }
+       DBG();
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());