From: Brian Norris <banorris@uci.edu>
Date: Tue, 18 Sep 2012 22:51:37 +0000 (-0700)
Subject: model: move init code to ModelChecker::initialize_curr_action
X-Git-Tag: pldi2013~177^2^2~8
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=cdf3ae3d7205018a412f75addf4113587a1a0586

model: move init code to ModelChecker::initialize_curr_action

Refactoring
---

diff --git a/model.cc b/model.cc
index e1e80fa..f2d4eb1 100644
--- a/model.cc
+++ b/model.cc
@@ -333,24 +333,8 @@ bool ModelChecker::process_write(ModelAction *curr)
 	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
- * calculates reads-from relationships, updates synchronization clock vectors,
- * forms a memory_order constraints graph, and handles replay/backtrack
- * execution when running permutations of previously-observed executions.
- *
- * @param curr The current action to process
- * @return The next Thread that must be executed. May be NULL if ModelChecker
- * makes no choice (e.g., according to replay execution, combining RMW actions,
- * etc.)
- */
-Thread * ModelChecker::check_current_action(ModelAction *curr)
+ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 {
-	ASSERT(curr);
-
-	bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
-
 	if (curr->is_rmwc() || curr->is_rmw()) {
 		ModelAction *tmp = process_rmw(curr);
 		delete curr;
@@ -383,6 +367,28 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 				compute_promises(curr);
 		}
 	}
+	return curr;
+}
+
+/**
+ * This is the heart of the model checker routine. It performs model-checking
+ * actions corresponding to a given "current action." Among other processes, it
+ * calculates reads-from relationships, updates synchronization clock vectors,
+ * forms a memory_order constraints graph, and handles replay/backtrack
+ * execution when running permutations of previously-observed executions.
+ *
+ * @param curr The current action to process
+ * @return The next Thread that must be executed. May be NULL if ModelChecker
+ * makes no choice (e.g., according to replay execution, combining RMW actions,
+ * etc.)
+ */
+Thread * ModelChecker::check_current_action(ModelAction *curr)
+{
+	ASSERT(curr);
+
+	bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
+
+	curr = initialize_curr_action(curr);
 
 	/* Thread specific actions */
 	switch (curr->get_type()) {
diff --git a/model.h b/model.h
index 030d7dd..b8a4859 100644
--- a/model.h
+++ b/model.h
@@ -112,6 +112,7 @@ private:
 	 */
 	void set_current_action(ModelAction *act) { priv->current_action = act; }
 	Thread * check_current_action(ModelAction *curr);
+	ModelAction * initialize_curr_action(ModelAction *curr);
 	bool process_read(ModelAction *curr, bool second_part_of_rmw);
 	bool process_write(ModelAction *curr);