From b6f06ab2c626eb6e0f044fa9c7d1b74fbc82a09d Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Mon, 8 Oct 2012 14:48:47 -0700
Subject: [PATCH] be even more aggressive about sleep sets... if an action was
 sleeping, it should only read from a value that could potentially result in
 synchronization with a release done while it was sleeping

---
 action.cc |  3 ++-
 action.h  |  5 +++++
 model.cc  | 26 +++++++++++++++++++++++---
 model.h   |  1 +
 4 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/action.cc b/action.cc
index c1adc2e..b7bf024 100644
--- a/action.cc
+++ b/action.cc
@@ -33,7 +33,8 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
 	reads_from(NULL),
 	node(NULL),
 	seq_number(ACTION_INITIAL_CLOCK),
-	cv(NULL)
+	cv(NULL),
+	sleep_flag(false)
 {
 	Thread *t = thread ? thread : thread_current();
 	this->tid = t->get_id();
diff --git a/action.h b/action.h
index 96b791e..68db2c3 100644
--- a/action.h
+++ b/action.h
@@ -125,6 +125,9 @@ public:
 	void process_rmw(ModelAction * act);
 	void copy_typeandorder(ModelAction * act);
 
+	void set_sleep_flag() { sleep_flag=true; }
+	bool get_sleep_flag() { return sleep_flag; }
+
 	MEMALLOC
 private:
 
@@ -155,6 +158,8 @@ private:
 	/** The clock vector stored with this action; only needed if this
 	 * action is a store release? */
 	ClockVector *cv;
+
+	bool sleep_flag;
 };
 
 typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;
diff --git a/model.cc b/model.cc
index d77ba4b..f8482cb 100644
--- a/model.cc
+++ b/model.cc
@@ -179,7 +179,6 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
 			tid = prevnode->get_next_backtrack();
 			/* Make sure the backtracked thread isn't sleeping. */
-			scheduler->remove_sleep(thread_map->get(id_to_int(tid)));
 			node_stack->pop_restofstack(1);
 			if (diverge==earliest_diverge) {
 				earliest_diverge=prevnode->get_action();
@@ -213,6 +212,7 @@ void ModelChecker::execute_sleep_set() {
 			thr->set_state(THREAD_RUNNING);
 			scheduler->next_thread(thr);
 			Thread::swap(&system_context, thr);
+			priv->current_action->set_sleep_flag();
 			thr->set_pending(priv->current_action);
 		}
 	}
@@ -346,7 +346,8 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	for(int i = low_tid; i < high_tid; i++) {
 		thread_id_t tid = int_to_id(i);
 
-		if (!node->is_enabled(tid))
+		/* Don't backtrack into a point where the thread is disabled or sleeping. */
+		if (node->get_enabled_array()[i]!=THREAD_ENABLED)
 			continue;
 	
 		/* Check if this has been explored already */
@@ -1846,7 +1847,12 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 					act->print();
 					curr->print();
 				}
-				curr->get_node()->add_read_from(act);
+
+				if (curr->get_sleep_flag()) {
+					if (sleep_can_read_from(curr, act))
+						curr->get_node()->add_read_from(act);
+				} else
+					curr->get_node()->add_read_from(act);
 			}
 
 			/* Include at most one act per-thread that "happens before" curr */
@@ -1873,6 +1879,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 	ASSERT(initialized);
 }
 
+bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
+	while(true) {
+		Node *prevnode=write->get_node()->get_parent();
+		bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+		if (write->is_release()&&thread_sleep)
+			return true;
+		if (!write->is_rmw())
+			return false;
+		if (write->get_reads_from()==NULL)
+			return true;
+		write=write->get_reads_from();
+	}
+}
+
 static void print_list(action_list_t *list)
 {
 	action_list_t::iterator it;
diff --git a/model.h b/model.h
index 1bd32a1..8316f04 100644
--- a/model.h
+++ b/model.h
@@ -118,6 +118,7 @@ private:
 	/** The scheduler to use: tracks the running/ready Threads */
 	Scheduler *scheduler;
 
+	bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
 	bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
 	bool has_asserted() {return asserted;}
 	void reset_asserted() {asserted=false;}
-- 
2.34.1