right fix for avoid rmw cycles... bad assumption in the cyclegraph

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index bd4ade23d540e371bb63ec7324ec933f7fb425db..015ca16796f9b9fdc9bae0ea0ff2b76dfdee4e7f 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -258,6 +258,7 @@ ModelAction * ModelChecker::get_next_backtrack()
        return next;
 }
 
+
 /**
  * Processes a read or rmw model action.
  * @param curr is the read model action to process.
@@ -275,8 +276,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
                        mo_graph->startChanges();
 
                        value = reads_from->get_value();
-                               /* Assign reads_from, perform release/acquire synchronization */
-                       curr->read_from(reads_from);
+
                        if (!second_part_of_rmw) {
                                check_recency(curr,false);
                        }
@@ -289,6 +289,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
                                continue;
                        }
 
+                       curr->read_from(reads_from);
                        mo_graph->commitChanges();
                        updated |= r_status;
                } else if (!second_part_of_rmw) {
@@ -457,7 +458,8 @@ bool ModelChecker::isfeasible() {
        return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
 }
 
-/** @returns whether the current partial trace is feasible. */
+/** @returns whether the current partial trace is feasible other than
+ * multiple RMW reading from the same store. */
 bool ModelChecker::isfeasibleotherthanRMW() {
        return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
 }
@@ -1040,6 +1042,8 @@ bool ModelChecker::resolve_promises(ModelAction *write)
        return resolved;
 }
 
+
+
 /**
  * Compute the set of promises that could potentially be satisfied by this
  * action. Note that the set computation actually appears in the Node, not in