experiment with exponential decay model

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 21207fefcb273a0bc0e4ab4a7b5fa4272691d71a..e1c5e2ddbb06767e13c51d55b230f553d5f2c67d 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -288,18 +288,18 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
        }
 
        // Remove writes that violate read modification order
-       for (uint i = 0; i < rf_set->size(); i++) {
+       uint i = 0;
+       while (i < rf_set->size()) {
                ModelAction * rf = (*rf_set)[i];
                if (!r_modification_order(curr, rf, NULL, NULL, true)) {
                        (*rf_set)[i] = rf_set->back();
                        rf_set->pop_back();
-               }
+               } else
+                       i++;
        }
 
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
-               if (index == -1)// no feasible write exists
-                       return false;
 
                ModelAction *rf = (*rf_set)[index];
 
@@ -318,6 +318,9 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                        }
                        return true;
                }
+
+               ASSERT(false);
+               /* TODO: Following code not needed anymore */
                priorset->clear();
                (*rf_set)[index] = rf_set->back();
                rf_set->pop_back();
@@ -718,12 +721,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        if (curr->is_read() && !second_part_of_rmw) {
                process_read(curr, rf_set);
                delete rf_set;
-
-/*             bool success = process_read(curr, rf_set);
-                delete rf_set;
-                if (!success)
-                        return curr;   // Do not add action to lists
- */
        } else
                ASSERT(rf_set == NULL);