From: bdemsky <bdemsky@uci.edu>
Date: Wed, 3 Jul 2019 23:24:12 +0000 (-0700)
Subject: Maintain list of writes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1c7618b4e8f7e85a85a2fb87252a3512b9493380;p=c11tester.git

Maintain list of writes
---

diff --git a/execution.cc b/execution.cc
index 8877fcdc..c9fb39f1 100644
--- a/execution.cc
+++ b/execution.cc
@@ -1065,6 +1065,10 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 		uninit = get_uninitialized_action(act);
 		uninit_id = id_to_int(uninit->get_tid());
 		list->push_front(uninit);
+		SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+		if (uninit_id >= (int)vec->size())
+			vec->resize(uninit_id + 1);
+		(*vec)[uninit_id].push_front(uninit);
 	}
 	list->push_back(act);
 
@@ -1110,6 +1114,12 @@ 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);
+
+	SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
+	int tid = id_to_int(write->get_tid());
+	if (tid >= (int)vec->size())
+		vec->resize(priv->next_thread_id);
+	(*vec)[tid].push_back(write);
 }
 
 /**
@@ -1252,7 +1262,7 @@ bool valequals(uint64_t val1, uint64_t val2, int size) {
  */
 SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
 {
-	SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
+	SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
 	unsigned int i;
 	ASSERT(curr->is_read());
 
@@ -1271,18 +1281,6 @@ SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *cu
 		for (rit = list->rbegin();rit != list->rend();rit++) {
 			ModelAction *act = *rit;
 
-			/* Only consider 'write' actions */
-			if (!act->is_write()) {
-				if (act != curr && act->is_read() && act->happens_before(curr)) {
-					ModelAction *tmp = act->get_reads_from();
-					if (((unsigned int) id_to_int(tmp->get_tid()))==i)
-						act = tmp;
-					else
-						break;
-				} else
-					continue;
-			}
-
 			if (act == curr)
 				continue;
 
diff --git a/execution.h b/execution.h
index 89b3200a..f8634ffa 100644
--- a/execution.h
+++ b/execution.h
@@ -143,6 +143,8 @@ private:
 
 	HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
 
+	HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_wr_thrd_map;
+
 	HashTable<const void *, ModelAction *, uintptr_t, 4> obj_last_sc_map;