X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=998059e2451e7e652d2493af3fc6785aad9ba542;hp=0bccd833ff843e40fd700f8ea3f198b1a2f4e065;hb=d5ec9d02d3ce4a92811a4515f808efcb0a1326b7;hpb=8d9a43be3bc794d7c9096dbda88640eb2fa99ee6

diff --git a/model.cc b/model.cc
index 0bccd833..998059e2 100644
--- a/model.cc
+++ b/model.cc
@@ -313,14 +313,41 @@ void ModelChecker::execute_sleep_set()
 	}
 }
 
+/**
+ * @brief Should the current action wake up a given thread?
+ *
+ * @param curr The current action
+ * @param thread The thread that we might wake up
+ * @return True, if we should wake up the sleeping thread; false otherwise
+ */
+bool ModelChecker::should_wake_up(const ModelAction *curr, const Thread *thread) const
+{
+	const ModelAction *asleep = thread->get_pending();
+	/* Don't allow partial RMW to wake anyone up */
+	if (curr->is_rmwr())
+		return false;
+	/* Synchronizing actions may have been backtracked */
+	if (asleep->could_synchronize_with(curr))
+		return true;
+	/* All acquire/release fences and fence-acquire/store-release */
+	if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
+		return true;
+	/* Fence-release + store can awake load-acquire on the same location */
+	if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
+		ModelAction *fence_release = get_last_fence_release(curr->get_tid());
+		if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
+			return true;
+	}
+	return false;
+}
+
 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
 {
 	for (unsigned int i = 0; i < get_num_threads(); i++) {
 		Thread *thr = get_thread(int_to_id(i));
 		if (scheduler->is_sleep_set(thr)) {
-			ModelAction *pending_act = thr->get_pending();
-			if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
-				//Remove this thread from sleep set
+			if (should_wake_up(curr, thr))
+				/* Remove this thread from sleep set */
 				scheduler->remove_sleep(thr);
 		}
 	}
@@ -545,25 +572,118 @@ bool ModelChecker::next_execution()
 	return true;
 }
 
-ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
+/**
+ * @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;
+
+	/* 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 */
+	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;
+
+		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: {
@@ -1870,7 +1990,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 	if (mo_graph->checkForCycles())
 		return false;
 
-	while (rf) {
+	for ( ; rf != NULL; rf = rf->get_reads_from()) {
 		ASSERT(rf->is_write());
 
 		if (rf->is_release())
@@ -1890,8 +2010,6 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 		/* acq_rel RMW is a sufficient stopping condition */
 		if (rf->is_acquire() && rf->is_release())
 			return true; /* complete */
-
-		rf = rf->get_reads_from();
 	};
 	if (!rf) {
 		/* read from future: need to settle this later */
@@ -2517,7 +2635,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
 bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
 {
-	while (true) {
+	for ( ; write != NULL; write = write->get_reads_from()) {
 		/* UNINIT actions don't have a Node, and they never sleep */
 		if (write->is_uninitialized())
 			return true;
@@ -2526,13 +2644,10 @@ bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *wri
 		bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
 		if (write->is_release() && thread_sleep)
 			return true;
-		if (!write->is_rmw()) {
+		if (!write->is_rmw())
 			return false;
-		}
-		if (write->get_reads_from() == NULL)
-			return true;
-		write = write->get_reads_from();
 	}
+	return true;
 }
 
 /**