From: Brian Norris <banorris@uci.edu>
Date: Thu, 28 Feb 2013 00:36:24 +0000 (-0800)
Subject: model: don't call process_read() for 2nd half of RMW/RMWC
X-Git-Tag: oopsla2013~213
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=61d1e3ae29b690f69cf77c5a6f836fb36507a694;p=model-checker.git

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 152e36e..417cbc1 100644
--- 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 783f7a6..9e0b34b 100644
--- 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);