right fix for avoid rmw cycles... bad assumption in the cyclegraph
[c11tester.git] / model.cc
index cc464a2bcc5b76b933d8769ba450486b4804edbf..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,9 +289,10 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
                                continue;
                        }
 
+                       curr->read_from(reads_from);
                        mo_graph->commitChanges();
                        updated |= r_status;
-               } else {
+               } else if (!second_part_of_rmw) {
                        /* Read from future value */
                        value = curr->get_node()->get_future_value();
                        modelclock_t expiration = curr->get_node()->get_future_value_expiration();
@@ -454,6 +455,12 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
+       return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
+}
+
+/** @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();
 }
 
@@ -704,9 +711,14 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                   =>
                                   that read could potentially read from our write.
                                 */
-                               if (isfeasible() && act->get_node()->add_future_value(curr->get_value(), curr->get_seq_number()+params.maxfuturedelay) &&
-                                               (!priv->next_backtrack || *act > *priv->next_backtrack))
-                                       priv->next_backtrack = act;
+                               if (thin_air_constraint_may_allow(curr, act)) {
+                                       if (isfeasible() ||
+                                                       (curr->is_rmw() && act->is_rmw() && curr->get_reads_from()==act->get_reads_from() && isfeasibleotherthanRMW())) {
+                                               if (act->get_node()->add_future_value(curr->get_value(), curr->get_seq_number()+params.maxfuturedelay) &&
+                                                               (!priv->next_backtrack || *act > *priv->next_backtrack))
+                                                       priv->next_backtrack = act;
+                                       }
+                               }
                        }
                }
        }
@@ -714,6 +726,29 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
        return added;
 }
 
+/** Arbitrary reads from the future are not allowed.  Section 29.3
+ * part 9 places some constraints.  This method checks one result of constraint
+ * constraint.  Others require compiler support. */
+
+bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
+       if (!writer->is_rmw())
+               return true;
+
+       if (!reader->is_rmw())
+               return true;
+
+       for(const ModelAction *search=writer->get_reads_from();search!=NULL;search=search->get_reads_from()) {
+               if (search==reader)
+                       return false;
+               if (search->get_tid()==reader->get_tid()&&
+                               search->happens_before(reader))
+                       break;
+       }
+
+       return true;
+}
+
+
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
  * The ModelAction under consideration is expected to be taking part in
@@ -988,6 +1023,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid)
 bool ModelChecker::resolve_promises(ModelAction *write)
 {
        bool resolved = false;
+
        for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
                Promise *promise = (*promises)[promise_index];
                if (write->get_node()->get_promise(i)) {
@@ -1003,10 +1039,11 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                } else
                        promise_index++;
        }
-
        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
@@ -1193,6 +1230,7 @@ bool ModelChecker::take_step() {
        if (curr) {
                if (curr->get_state() == THREAD_READY) {
                        ASSERT(priv->current_action);
+
                        priv->nextThread = check_current_action(priv->current_action);
                        priv->current_action = NULL;
                        if (!curr->is_blocked() && !curr->is_complete())