X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=e0edbec091bcba052b926c560dec5a306fe8bee4;hp=a5ac71316e2f2dc69e469d9d99a6ffee941a072e;hb=7064cf5c139946885b0d3df46f59da4946b34d4c;hpb=25728e9ac2afc0ecfb23259a6cee27a309027f4f

diff --git a/model.cc b/model.cc
index a5ac7131..e0edbec0 100644
--- a/model.cc
+++ b/model.cc
@@ -545,25 +545,112 @@ bool ModelChecker::next_execution()
 	return true;
 }
 
+/**
+ * @brief Find the last fence-related backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking, as affected by fence
+ * operations. This includes pairs of potentially-synchronizing actions which
+ * occur due to fence-acquire or fence-release, and hence should be explored in
+ * the opposite execution order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act due to fences
+ */
+ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
+{
+	/* Only perform release/acquire fence backtracking for stores */
+	if (!act->is_write())
+		return NULL;
+
+	/* Find a fence-release (or, act is a release) */
+	ModelAction *last_release;
+	if (act->is_release())
+		last_release = act;
+	else
+		last_release = get_last_fence_release(act->get_tid());
+	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;
+	/* 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++) {
+		ModelAction *prev = *rit;
+		if (act->same_thread(prev))
+			continue;
+
+		int tid = id_to_int(prev->get_tid());
+
+		if (prev->is_read() && act->same_var(prev)) {
+			if (prev->is_acquire()) {
+				/* Found most recent load-acquire, don't need
+				 * to search for more fences */
+				if (!found_acquire_fences)
+					return NULL;
+			} else {
+				prior_loads[tid] = prev;
+			}
+		}
+		if (prev->is_acquire() && prev->is_fence() && !acquire_fences[tid]) {
+			found_acquire_fences = true;
+			acquire_fences[tid] = prev;
+		}
+	}
+
+	ModelAction *latest_backtrack = NULL;
+	for (unsigned int i = 0; i < acquire_fences.size(); i++)
+		if (acquire_fences[i] && prior_loads[i])
+			if (!latest_backtrack || *latest_backtrack < *acquire_fences[i])
+				latest_backtrack = acquire_fences[i];
+	return latest_backtrack;
+}
+
+/**
+ * @brief Find the last backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking. This primary includes pairs of
+ * synchronizing actions which should be explored in the opposite execution
+ * order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act
+ */
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act) const
 {
 	switch (act->get_type()) {
-	case ATOMIC_FENCE:
+	/* case ATOMIC_FENCE: fences don't directly cause backtracking */
 	case ATOMIC_READ:
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {
-		/* Optimization: relaxed operations don't need backtracking */
-		if (act->is_relaxed())
-			return NULL;
+		ModelAction *ret = NULL;
+
 		/* linear search: from most recent to oldest */
 		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
-			if (prev->could_synchronize_with(act))
-				return prev;
+			if (prev->could_synchronize_with(act)) {
+				ret = prev;
+				break;
+			}
 		}
-		break;
+
+		ModelAction *ret2 = get_last_fence_conflict(act);
+		if (!ret2)
+			return ret;
+		if (!ret)
+			return ret2;
+		if (*ret < *ret2)
+			return ret2;
+		return ret;
 	}
 	case ATOMIC_LOCK:
 	case ATOMIC_TRYLOCK: {