model: don't call process_read() for 2nd half of RMW/RMWC

We don't need to call process_read() for the second half of an RMW or
RMWC ModelAction. Anyway, it does next-to-nothing when
'second_part_of_rmw' is true.

diff --git a/model.cc b/model.cc
index 152e36ec2f296fc9f467b890e2e89d6ada3504ee..417cbc1cf05ee95dffb3bb37180f56fd9d0bcd9e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -842,12 +842,11 @@ ModelAction * ModelChecker::get_next_backtrack()
 }
 
 /**
- * Processes a read or rmw model action.
+ * Processes a read model action.
  * @param curr is the read model action to process.
- * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
  * @return True if processing this read updates the mo_graph.
  */
-bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
+bool ModelChecker::process_read(ModelAction *curr)
 {
        uint64_t value = VALUE_NONE;
        bool updated = false;
@@ -857,14 +856,11 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                        mo_graph->startChanges();
 
                        value = reads_from->get_value();
-                       bool r_status = false;
 
-                       if (!second_part_of_rmw) {
-                               check_recency(curr, reads_from);
-                               r_status = r_modification_order(curr, reads_from);
-                       }
+                       check_recency(curr, reads_from);
+                       bool r_status = r_modification_order(curr, reads_from);
 
-                       if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
+                       if (is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
                                mo_graph->rollbackChanges();
                                priv->too_many_reads = false;
                                continue;
@@ -875,7 +871,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                        mo_check_promises(curr, true);
 
                        updated |= r_status;
-               } else if (!second_part_of_rmw) {
+               } else {
                        /* Read from future value */
                        struct future_value fv = curr->get_node()->get_future_value();
                        Promise *promise = new Promise(curr, fv);
@@ -1437,7 +1433,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
                        if (process_thread_action(curr))
                                update_all = true;
 
-                       if (act->is_read() && process_read(act, second_part_of_rmw))
+                       if (act->is_read() && !second_part_of_rmw && process_read(act))
                                update = true;
 
                        if (act->is_write() && process_write(act))

diff --git a/model.h b/model.h
index 783f7a6623df79d89d9611214393098e95484a9a..9e0b34ba18b25cf642a92dea56321763c23b48ba 100644 (file)
--- a/model.h
+++ b/model.h
@@ -155,7 +155,7 @@ private:
        bool next_execution();
        ModelAction * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
-       bool process_read(ModelAction *curr, bool second_part_of_rmw);
+       bool process_read(ModelAction *curr);
        bool process_write(ModelAction *curr);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);