From: Brian Norris <banorris@uci.edu>
Date: Thu, 21 Feb 2013 19:59:50 +0000 (-0800)
Subject: model: only backtrack fences when acquire is before release
X-Git-Tag: oopsla2013~235
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=a01fa7fb82f22ef8d4787fd5d3ad44598a44f924

model: only backtrack fences when acquire is before release

Because there are up to 4 actions involved in this search for a
"conflict" (load, fence-acquire, fence-release, store), I overlooked the
fact that we only need to backtrack when the release comes after acquire
in the execution order. This fix skips past the 'release' action before
we begin searching for the 'acquire'.
---

diff --git a/model.cc b/model.cc
index e0edbec..8f0b3ce 100644
--- a/model.cc
+++ b/model.cc
@@ -572,16 +572,22 @@ ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
 	if (!last_release)
 		return NULL;
 
-	std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
-	std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
-	bool found_acquire_fences = false;
+	/* Skip past the release */
+	action_list_t *list = action_trace;
+	action_list_t::reverse_iterator rit;
+	for (rit = list->rbegin(); rit != list->rend(); rit++)
+		if (*rit == last_release)
+			break;
+	ASSERT(rit != list->rend());
+
 	/* Find a prior:
 	 *   load-acquire
 	 * or
 	 *   load --sb-> fence-acquire */
-	action_list_t *list = action_trace;
-	action_list_t::reverse_iterator rit;
-	for (rit = list->rbegin(); rit != list->rend(); rit++) {
+	std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
+	std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
+	bool found_acquire_fences = false;
+	for ( ; rit != list->rend(); rit++) {
 		ModelAction *prev = *rit;
 		if (act->same_thread(prev))
 			continue;