From f4027c4b37866d298960390f13febd906f05b8e7 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 3 Jul 2019 16:08:15 -0700
Subject: [PATCH] Optimize SC lookup

---
 action.h     |  4 ++--
 execution.cc | 26 +++++++++++++-------------
 execution.h  |  3 ++-
 model.cc     | 22 +++++++++++-----------
 4 files changed, 28 insertions(+), 27 deletions(-)

diff --git a/action.h b/action.h
index 4eb1f7ed..5862485b 100644
--- 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 de7cfa2f..8877fcdc 100644
--- 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 150fc68b..89b3200a 100644
--- 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 3b4784d2..17916954 100644
--- 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());
-- 
2.34.1