From a743578aadfe36cd90d7f9176e04410473c55b93 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Sep 2012 16:16:30 -0700
Subject: [PATCH] model: more restructuring of read/write processing

Make a ModelChecker::process_write function, for symmetry and to shorten the
code portions where the main control flow happens.
---
 model.cc | 50 +++++++++++++++++++++++++++++---------------------
 model.h  |  1 +
 2 files changed, 30 insertions(+), 21 deletions(-)

diff --git a/model.cc b/model.cc
index 80cbbe0..79c52d0 100644
--- a/model.cc
+++ b/model.cc
@@ -305,6 +305,31 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 	}
 }
 
+/**
+ * Process a write ModelAction
+ * @param curr The ModelAction to process
+ * @return True if the mo_graph was updated or promises were resolved
+ */
+bool ModelChecker::process_write(ModelAction *curr)
+{
+	bool updated_mod_order = w_modification_order(curr);
+	bool updated_promises = resolve_promises(curr);
+
+	if (promises->size() == 0) {
+		for (unsigned int i = 0; i<futurevalues->size(); i++) {
+			struct PendingFutureValue pfv = (*futurevalues)[i];
+			if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
+					(!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
+				priv->next_backtrack = pfv.act;
+		}
+		futurevalues->resize(0);
+	}
+
+	mo_graph->commitChanges();
+	get_thread(curr)->set_return_value(VALUE_NONE);
+	return updated_mod_order || updated_promises;
+}
+
 /**
  * This is the heart of the model checker routine. It performs model-checking
  * actions corresponding to a given "current action." Among other processes, it
@@ -394,28 +419,11 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	bool updated = false;
 
-	if (curr->is_read()) {
-		updated = process_read(curr, second_part_of_rmw);
-	}
+	if (curr->is_read() && process_read(curr, second_part_of_rmw))
+		updated = true;
 
-	if (curr->is_write()) {
-		bool updated_mod_order = w_modification_order(curr);
-		bool updated_promises = resolve_promises(curr);
-		updated = updated || updated_mod_order || updated_promises;
-
-		if (promises->size()==0) {
-			for (unsigned int i = 0; i<futurevalues->size(); i++) {
-				struct PendingFutureValue pfv=(*futurevalues)[i];
-				if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
-						(!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
-					priv->next_backtrack = pfv.act;
-			}
-			futurevalues->resize(0);
-		}
-
-		mo_graph->commitChanges();
-		get_thread(curr)->set_return_value(VALUE_NONE);
-	}
+	if (curr->is_write() && process_write(curr))
+		updated = true;
 
 	if (updated)
 		resolve_release_sequences(curr->get_location());
diff --git a/model.h b/model.h
index 7db1a8d..248e164 100644
--- a/model.h
+++ b/model.h
@@ -111,6 +111,7 @@ private:
 	void set_current_action(ModelAction *act) { priv->current_action = act; }
 	Thread * check_current_action(ModelAction *curr);
 	bool process_read(ModelAction *curr, bool second_part_of_rmw);
+	bool process_write(ModelAction *curr);
 
 	bool take_step();
 
-- 
2.34.1