From: Brian Norris <banorris@uci.edu>
Date: Sat, 2 Mar 2013 08:04:44 +0000 (-0800)
Subject: check_recency: only allow newer stores to "overwrite"
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=284151d644be0946f887561a03344866f0665c03

check_recency: only allow newer stores to "overwrite"

For a "live" memory system, we only want to force a store to appear if
it is modification-ordered after the store we're reading from.

Also, delete my old comment about reads-from feasibility.
---

diff --git a/model.cc b/model.cc
index fba9cf00..36c23bf1 100644
--- a/model.cc
+++ b/model.cc
@@ -1694,11 +1694,9 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 		if (write == rf)
 			continue;
 
-		//NOTE: SHOULD MAKE SURE write is MOd after rf
-
-		/* Test to see whether this is a feasible write to read from */
-		/** NOTE: all members of read-from set should be
-		 *  feasible, so we no longer check it here **/
+		/* Only look for "newer" writes */
+		if (!mo_graph->checkReachable(rf, write))
+			continue;
 
 		ritcopy = rit;