check_recency: only allow newer stores to "overwrite"

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index d523fc29ad786a861d0eca41eb0a3bd93dfa4991..36c23bf1c17e6a56e73ab62001344aa630c32122 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1694,27 +1694,17 @@ 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;
 
                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;
-                       bool foundvalue = false;
-                       for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
-                               if (act->get_node()->get_read_from_past(j) == write) {
-                                       foundvalue = true;
-                                       break;
-                               }
-                       }
-                       if (!foundvalue) {
+                       if (!act->may_read_from(write)) {
                                feasiblewrite = false;
                                break;
                        }