remove extra cyclegraph calls

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index a6ed9d689b5b632bf1d14eae241272283c0d47a2..3a994892b7102692ea0423d8cc572cc00ed10163 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -285,18 +285,26 @@ bool ModelExecution::is_complete_execution() const
  */
 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
 {
-       bool updated = false;
+  while(true) {
                
-       const ModelAction *rf = fuzzer->selectWrite(curr, rf_set);
-
-       ASSERT(rf);
-       
-       mo_graph->startChanges();
-       updated = r_modification_order(curr, rf);
-       read_from(curr, rf);
-       mo_graph->commitChanges();
-       get_thread(curr)->set_return_value(curr->get_return_value());
-       return updated;
+    int index = fuzzer->selectWrite(curr, rf_set);
+    const ModelAction *rf = (*rf_set)[index];
+
+    
+    ASSERT(rf);
+    
+    mo_graph->startChanges();
+    bool updated = r_modification_order(curr, rf);
+    if (!is_infeasible()) {
+      read_from(curr, rf);
+      mo_graph->commitChanges();
+      get_thread(curr)->set_return_value(curr->get_return_value());
+      return updated;
+    }
+    mo_graph->rollbackChanges();
+    (*rf_set)[index] = rf_set->back();
+    rf_set->pop_back();
+  }
 }
 
 /**
@@ -698,6 +706,8 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        if (curr->is_read() && !second_part_of_rmw) {
          process_read(curr, rf_set);
          delete rf_set;
+       } else {
+         ASSERT(rf_set == NULL);
        }
        
        if (curr->is_write())
@@ -1294,6 +1304,22 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const
        return get_parent_action(tid)->get_cv();
 }
 
+bool valequals(uint64_t val1, uint64_t val2, int size) {
+  switch(size) {
+  case 1:
+    return ((uint8_t)val1) == ((uint8_t)val2);
+  case 2:
+    return ((uint16_t)val1) == ((uint16_t)val2);
+  case 4:
+    return ((uint32_t)val1) == ((uint32_t)val2);
+  case 8:
+    return val1==val2;
+  default:
+    ASSERT(0);
+    return false;
+  }
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from, as well as any previously-observed future values that must still be valid.
@@ -1332,6 +1358,20 @@ ModelVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *c
                        if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
                                allow_read = false;
 
+                       /* Need to check whether we will have two RMW reading from the same value */
+                       if (curr->is_rmwr()) {
+                         /* It is okay if we have a failing CAS */
+                         if (!curr->is_rmwrcas() ||
+                             valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+                               //Need to make sure we aren't the second RMW
+                               CycleNode * node = mo_graph->getNode_noCreate(act);
+                               if (node != NULL && node->getRMW() != NULL) {
+                                 //we are the second RMW
+                                 allow_read = false;
+                               }
+                             }
+                       }
+                       
                        if (allow_read) {
                                /* Only add feasible reads */
                                mo_graph->startChanges();