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 fba9cf00c7288f003a208356b4edeb6302748fcf..36c23bf1c17e6a56e73ab62001344aa630c32122 100644 (file)
--- 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;