check_recency: only allow newer stores to "overwrite"

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index a7ff82b474fa0c4aff711f82f2cdc7de7608b719..36c23bf1c17e6a56e73ab62001344aa630c32122 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1655,37 +1655,32 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 {
        if (!params.maxreads)
                return;
+
+       //NOTE: Next check is just optimization, not really necessary....
        if (curr->get_node()->get_read_from_past_size() <= 1)
                return;
        /* Must make sure that execution is currently feasible...  We could
         * accidentally clear by rolling back */
        if (is_infeasible())
                return;
+
        std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
        int tid = id_to_int(curr->get_tid());
-
-       /* Skip checks */
-       if ((int)thrd_lists->size() <= tid)
-               return;
+       ASSERT(tid < (int)thrd_lists->size());
        action_list_t *list = &(*thrd_lists)[tid];
-
        action_list_t::reverse_iterator rit = list->rbegin();
+       ASSERT((*rit) == curr);
        /* Skip past curr */
-       for (; (*rit) != curr; rit++)
-               ;
-       /* go past curr now */
        rit++;
 
        action_list_t::reverse_iterator ritcopy = rit;
        /* See if we have enough reads from the same value */
-       int count = 0;
-       for (; count < params.maxreads; rit++, count++) {
-               if (rit == list->rend())
+       for (int count = 0; count < params.maxreads; ritcopy++, count++) {
+               if (ritcopy == list->rend())
                        return;
-               ModelAction *act = *rit;
+               ModelAction *act = *ritcopy;
                if (!act->is_read())
                        return;
-
                if (act->get_reads_from() != rf)
                        return;
                if (act->get_node()->get_read_from_past_size() <= 1)
@@ -1699,25 +1694,17 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
                if (write == rf)
                        continue;
 
-               /* 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;
 
-               rit = ritcopy;
+               ritcopy = rit;
 
                bool feasiblewrite = true;
                /* now we need to see if this write works for everyone */
-
-               for (int loop = count; loop > 0; loop--, rit++) {
-                       ModelAction *act = *rit;
-                       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) {
+               for (int loop = params.maxreads; loop > 0; loop--, ritcopy++) {
+                       ModelAction *act = *ritcopy;
+                       if (!act->may_read_from(write)) {
                                feasiblewrite = false;
                                break;
                        }