From: Brian Norris <banorris@uci.edu>
Date: Tue, 18 Sep 2012 23:42:09 +0000 (-0700)
Subject: model: add curr to action lists early
X-Git-Tag: pldi2013~177^2^2~4
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=502c7029755b194e52526fe26c2e7327b5d64101

model: add curr to action lists early

The current action should be added to the ModelChecker lists early within
check_current_action, so that we can have consistency throughout the function.
We only allow an isolated piece of initialization (initialize_curr_action) to
occur before this step.
---

diff --git a/model.cc b/model.cc
index ebadbb6..e41bc4e 100644
--- a/model.cc
+++ b/model.cc
@@ -400,6 +400,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	ModelAction *newcurr = initialize_curr_action(curr);
 
+	/* Add the action to lists before any other model-checking tasks */
+	if (!second_part_of_rmw)
+		add_action_to_lists(newcurr);
+
 	/* Build may_read_from set for newly-created actions */
 	if (curr == newcurr && curr->is_read())
 		build_reads_from_past(curr);
@@ -440,10 +444,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		break;
 	}
 
-	/* Add current action to lists before work_queue loop */
-	if (!second_part_of_rmw)
-		add_action_to_lists(curr);
-
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
 
 	while (!work_queue.empty()) {