another bug fix...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index bd4ade23d540e371bb63ec7324ec933f7fb425db..c3a8c8415a71ed684e18b19fc2e9284e6bc6fac1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -34,7 +34,8 @@ ModelChecker::ModelChecker(struct model_params params) :
        mo_graph(new CycleGraph()),
        failed_promise(false),
        too_many_reads(false),
-       asserted(false)
+       asserted(false),
+       rmw_cycle(false)
 {
        /* Allocate this "size" on the snapshotting heap */
        priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -77,6 +78,7 @@ void ModelChecker::reset_to_initial_state()
        node_stack->reset_execution();
        failed_promise = false;
        too_many_reads = false;
+       rmw_cycle=false;
        reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
 }
@@ -258,6 +260,30 @@ ModelAction * ModelChecker::get_next_backtrack()
        return next;
 }
 
+
+/** Checks whether making the ModelAction read read_from the
+               ModelAction write will introduce a cycle in the reads_from
+               relation.
+
+@return true if making it read from will be fine, false otherwise.
+
+*/
+
+bool ModelChecker::ensure_rmw_acyclic(const ModelAction * read, const ModelAction *write) {
+       if (!read->is_rmw())
+               return true;
+       if (!write->is_rmw())
+               return true;
+       while(write!=NULL) {
+               if (write==read) {
+                       rmw_cycle=true;
+                       return false;
+               }
+               write=write->get_reads_from();
+       }
+       return true;
+}
+
 /**
  * Processes a read or rmw model action.
  * @param curr is the read model action to process.
@@ -276,7 +302,8 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
 
                        value = reads_from->get_value();
                                /* Assign reads_from, perform release/acquire synchronization */
-                       curr->read_from(reads_from);
+                       if (ensure_rmw_acyclic(curr, reads_from))
+                               curr->read_from(reads_from);
                        if (!second_part_of_rmw) {
                                check_recency(curr,false);
                        }
@@ -457,9 +484,10 @@ 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();
+       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !rmw_cycle && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -1026,7 +1054,8 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                Promise *promise = (*promises)[promise_index];
                if (write->get_node()->get_promise(i)) {
                        ModelAction *read = promise->get_action();
-                       read->read_from(write);
+                       if (ensure_rmw_acyclic(read, write))
+                               read->read_from(write);
                        if (read->is_rmw()) {
                                mo_graph->addRMWEdge(write, read);
                        }
@@ -1040,6 +1069,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