From: Brian Norris <banorris@uci.edu>
Date: Fri, 22 Feb 2013 07:07:55 +0000 (-0800)
Subject: model: wake up pending (sleep-set) actions for fences
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=d5ec9d02d3ce4a92811a4515f808efcb0a1326b7

model: wake up pending (sleep-set) actions for fences

This completes fence backtracking properly by waking up actions when the
appropriate fence interactions occur. This is a little more complicated
than the simple "could_synchronize()" test, since fence synchronization
can involve interaction of more than two actions.

So, pull the complexity of the "should we wake a thread up" computation
into its own function.
---

diff --git a/model.cc b/model.cc
index 8f0b3ce4..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);
 		}
 	}
diff --git a/model.h b/model.h
index de1fc639..bb548c22 100644
--- a/model.h
+++ b/model.h
@@ -149,6 +149,7 @@ private:
 	void set_bad_synchronization();
 	bool promises_expired() const;
 	void execute_sleep_set();
+	bool should_wake_up(const ModelAction *curr, const Thread *thread) const;
 	void wake_up_sleeping_actions(ModelAction *curr);
 	modelclock_t get_next_seq_num();