From: Brian Norris <banorris@uci.edu>
Date: Sat, 2 Mar 2013 09:02:29 +0000 (-0800)
Subject: check_recency: refactor some more, + include Promises
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=745b71256a4b96ddf4843c7f66b11d0cb3daa3cb

check_recency: refactor some more, + include Promises

check_recency *should* now prevent reading from the same Promise too
many times. Not quite getting the test results I want yet, though.
---

diff --git a/model.cc b/model.cc
index a0df0876..b0ca05ea 100644
--- a/model.cc
+++ b/model.cc
@@ -1642,6 +1642,33 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 	return lastread;
 }
 
+template <typename T>
+bool ModelChecker::should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const
+{
+	/* Need a different write/promise */
+	if (other_rf->equals(rf))
+		return false;
+
+	/* Only look for "newer" writes/promises */
+	if (!mo_graph->checkReachable(rf, other_rf))
+		return false;
+
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+	action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())];
+	action_list_t::reverse_iterator rit = list->rbegin();
+	ASSERT((*rit) == curr);
+	/* Skip past curr */
+	rit++;
+
+	/* Does this write/promise work for everyone? */
+	for (int i = 0; i < params.maxreads; i++, rit++) {
+		ModelAction *act = *rit;
+		if (!act->may_read_from(other_rf))
+			return false;
+	}
+	return true;
+}
+
 /**
  * Checks whether a thread has read from the same write for too many times
  * without seeing the effects of a later write.
@@ -1663,7 +1690,8 @@ bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const
 		return true;
 
 	//NOTE: Next check is just optimization, not really necessary....
-	if (curr->get_node()->get_read_from_past_size() <= 1)
+	if (curr->get_node()->get_read_from_past_size() +
+			curr->get_node()->get_read_from_promise_size() <= 1)
 		return true;
 
 	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
@@ -1683,36 +1711,23 @@ bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const
 		ModelAction *act = *ritcopy;
 		if (!act->is_read())
 			return true;
-		if (act->get_reads_from() != rf)
+		if (act->get_reads_from_promise() && !act->get_reads_from_promise()->equals(rf))
 			return true;
-		if (act->get_node()->get_read_from_past_size() <= 1)
+		if (act->get_reads_from() && !act->get_reads_from()->equals(rf))
+			return true;
+		if (act->get_node()->get_read_from_past_size() +
+				act->get_node()->get_read_from_promise_size() <= 1)
 			return true;
 	}
 	for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
-		/* Get write */
 		const ModelAction *write = curr->get_node()->get_read_from_past(i);
-
-		/* Need a different write */
-		if (write == rf)
-			continue;
-
-		/* Only look for "newer" writes */
-		if (!mo_graph->checkReachable(rf, write))
-			continue;
-
-		ritcopy = rit;
-
-		bool feasiblewrite = true;
-		/* now we need to see if this write works for everyone */
-		for (int loop = params.maxreads; loop > 0; loop--, ritcopy++) {
-			ModelAction *act = *ritcopy;
-			if (!act->may_read_from(write)) {
-				feasiblewrite = false;
-				break;
-			}
-		}
-		if (feasiblewrite)
-			return false;
+		if (should_read_instead(curr, rf, write))
+			return false; /* liveness failure */
+	}
+	for (int i = 0; i < curr->get_node()->get_read_from_promise_size(); i++) {
+		const Promise *promise = curr->get_node()->get_read_from_promise(i);
+		if (should_read_instead(curr, rf, promise))
+			return false; /* liveness failure */
 	}
 	return true;
 }
diff --git a/model.h b/model.h
index 115d9445..3f4ca001 100644
--- a/model.h
+++ b/model.h
@@ -168,6 +168,10 @@ private:
 	Thread * take_step(ModelAction *curr);
 
 	bool check_recency(ModelAction *curr, const ModelAction *rf) const;
+
+	template <typename T>
+	bool should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const;
+
 	ModelAction * get_last_fence_conflict(ModelAction *act) const;
 	ModelAction * get_last_conflict(ModelAction *act) const;
 	void set_backtracking(ModelAction *act);