From: Brian Norris <banorris@uci.edu>
Date: Fri, 14 Sep 2012 19:43:25 +0000 (-0700)
Subject: model: fixup happens_before/reflexivity, add 'curr' to lists earlier
X-Git-Tag: pldi2013~177^2^2~12^2~4
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=22cfbcda627e74a3a8134bfcde03793e18c47681

model: fixup happens_before/reflexivity, add 'curr' to lists earlier

Some code under 'check_current_action' assumes that the current action is not
added to the ModelChecker trace/list data structures yet. However, some
features I need to add will require the current action to be in these
data structures already. So there are a few spots I need to fixup so that the
code can handle "happens_before" reflexivity properly.

This commit moves the "add_action_to_lists()" call as well as fixes up
reflexivity.
---

diff --git a/model.cc b/model.cc
index 954c07d..acd2079 100644
--- a/model.cc
+++ b/model.cc
@@ -420,6 +420,10 @@ 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()) {
@@ -451,10 +455,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		}
 	}
 
-	/* Add action to list.  */
-	if (!second_part_of_rmw)
-		add_action_to_lists(curr);
-
 	check_curr_backtracking(curr);
 
 	set_backtracking(curr);
@@ -648,8 +648,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *act = *rit;
 
-			/* Include at most one act per-thread that "happens before" curr */
-			if (act->happens_before(curr)) {
+			/*
+			 * Include at most one act per-thread that "happens
+			 * before" curr. Don't consider reflexively.
+			 */
+			if (act->happens_before(curr) && act != curr) {
 				if (act->is_write()) {
 					if (rf != act && act != curr) {
 						mo_graph->addEdge(act, rf);
@@ -770,8 +773,12 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *act = *rit;
 
-			/* Include at most one act per-thread that "happens before" curr */
-			if (act->happens_before(curr)) {
+			/*
+			 * Include at most one act per-thread that "happens
+			 * before" curr. Only consider reflexively if curr is
+			 * RMW.
+			 */
+			if (act->happens_before(curr) && (act != curr || curr->is_rmw())) {
 				/*
 				 * Note: if act is RMW, just add edge:
 				 *   act --mo--> curr