From 59eb730e1d19a0825008c40eb521bfc5c29df5f9 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Mon, 8 Oct 2012 01:15:06 -0700
Subject: [PATCH] add support for sleep sets...

---
 action.cc    |  2 ++
 model.cc     | 61 +++++++++++++++++++++++++++++++++++++++++++---------
 model.h      |  3 ++-
 nodestack.cc |  4 ++--
 nodestack.h  |  1 +
 schedule.cc  | 36 ++++++++++++++++++++++++++++++-
 schedule.h   |  6 +++++-
 7 files changed, 98 insertions(+), 15 deletions(-)

diff --git a/action.cc b/action.cc
index b4f4e43..8dba82f 100644
--- a/action.cc
+++ b/action.cc
@@ -8,6 +8,7 @@
 #include "clockvector.h"
 #include "common.h"
 #include "threads.h"
+#include "nodestack.h"
 
 #define ACTION_INITIAL_CLOCK 0
 
@@ -17,6 +18,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint
 	location(loc),
 	value(value),
 	reads_from(NULL),
+	node(NULL),
 	seq_number(ACTION_INITIAL_CLOCK),
 	cv(NULL)
 {
diff --git a/model.cc b/model.cc
index c3f6372..2c27567 100644
--- a/model.cc
+++ b/model.cc
@@ -150,6 +150,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			earliest_diverge=diverge;
 
 		Node *nextnode = next->get_node();
+		Node *prevnode = nextnode->get_parent();
+		scheduler->update_sleep_set(prevnode);
+
 		/* Reached divergence point */
 		if (nextnode->increment_promise()) {
 			/* The next node will try to satisfy a different set of promises. */
@@ -165,13 +168,18 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			node_stack->pop_restofstack(2);
 		} else {
 			/* Make a different thread execute for next step */
-			Node *node = nextnode->get_parent();
-			tid = node->get_next_backtrack();
+			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=node->get_action();
+				earliest_diverge=prevnode->get_action();
 			}
 		}
+		/* The correct sleep set is in the parent node. */
+		execute_sleep_set();
+
 		DEBUG("*** Divergence point ***\n");
 
 		diverge = NULL;
@@ -183,6 +191,40 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 	return thread_map->get(id_to_int(tid));
 }
 
+/** 
+ * We need to know what the next actions of all threads in the sleep
+ * set will be.  This method computes them and stores the actions at
+ * the corresponding thread object's pending action.
+ */
+
+void ModelChecker::execute_sleep_set() {
+	for(unsigned int i=0;i<get_num_threads();i++) {
+		thread_id_t tid=int_to_id(i);
+		Thread *thr=get_thread(tid);
+		if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
+			thr->set_state(THREAD_RUNNING);
+			scheduler->next_thread(thr);
+			Thread::swap(&system_context, thr);
+			thr->set_pending(priv->current_action);
+		}
+	}
+	priv->current_action = NULL;
+}
+
+void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
+	for(unsigned int i=0;i<get_num_threads();i++) {
+		thread_id_t tid=int_to_id(i);
+		Thread *thr=get_thread(tid);
+		if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
+			ModelAction *pending_act=thr->get_pending();
+			if (pending_act->could_synchronize_with(curr)) {
+				//Remove this thread from sleep set
+				scheduler->remove_sleep(thr);
+			}
+		}
+	}	
+}
+
 /**
  * Queries the model-checker for more executions to explore and, if one
  * exists, resets the model-checker state to execute a new execution.
@@ -270,7 +312,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 	return NULL;
 }
 
-/** This method find backtracking points where we should try to
+/** This method finds backtracking points where we should try to
  * reorder the parameter ModelAction against.
  *
  * @param the ModelAction to find backtracking points for.
@@ -295,9 +337,10 @@ 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))
 			continue;
-
+	
 		/* Check if this has been explored already */
 		if (node->has_been_explored(tid))
 			continue;
@@ -315,7 +358,6 @@ void ModelChecker::set_backtracking(ModelAction *act)
 			if (unfair)
 				continue;
 		}
-
 		/* Cache the latest backtracking point */
 		if (!priv->next_backtrack || *prev > *priv->next_backtrack)
 			priv->next_backtrack = prev;
@@ -631,7 +673,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 Thread * ModelChecker::check_current_action(ModelAction *curr)
 {
 	ASSERT(curr);
-
 	bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
 
 	if (!check_action_enabled(curr)) {
@@ -642,8 +683,11 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		return get_next_thread(NULL);
 	}
 
+	wake_up_sleeping_actions(curr);
+
 	ModelAction *newcurr = initialize_curr_action(curr);
 
+
 	/* Add the action to lists before any other model-checking tasks */
 	if (!second_part_of_rmw)
 		add_action_to_lists(newcurr);
@@ -655,7 +699,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
-
 	while (!work_queue.empty()) {
 		WorkQueueEntry work = work_queue.front();
 		work_queue.pop_front();
@@ -714,9 +757,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	}
 
 	check_curr_backtracking(curr);
-
 	set_backtracking(curr);
-
 	return get_next_thread(curr);
 }
 
diff --git a/model.h b/model.h
index d5dc422..d2baaf4 100644
--- a/model.h
+++ b/model.h
@@ -124,7 +124,8 @@ private:
 	int num_executions;
 	int num_feasible_executions;
 	bool promises_expired();
-
+	void execute_sleep_set();
+	void wake_up_sleeping_actions(ModelAction * curr);
 	modelclock_t get_next_seq_num();
 
 	/**
diff --git a/nodestack.cc b/nodestack.cc
index 4cf8950..76d167d 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -265,13 +265,13 @@ thread_id_t Node::get_next_backtrack()
 bool Node::is_enabled(Thread *t)
 {
 	int thread_id=id_to_int(t->get_id());
-	return thread_id < num_threads && (enabled_array[thread_id] == THREAD_ENABLED);
+	return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
 }
 
 bool Node::is_enabled(thread_id_t tid)
 {
 	int thread_id=id_to_int(tid);
-	return thread_id < num_threads && (enabled_array[thread_id] == THREAD_ENABLED);
+	return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
 }
 
 bool Node::has_priority(thread_id_t tid)
diff --git a/nodestack.h b/nodestack.h
index 55deac5..147b004 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -90,6 +90,7 @@ public:
 	bool get_promise(unsigned int i);
 	bool increment_promise();
 	bool promise_empty();
+	enabled_type_t *get_enabled_array() {return enabled_array;}
 
 	void print();
 	void print_may_read_from();
diff --git a/schedule.cc b/schedule.cc
index a236bd0..c5e58fe 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -5,6 +5,7 @@
 #include "schedule.h"
 #include "common.h"
 #include "model.h"
+#include "nodestack.h"
 
 /** Constructor */
 Scheduler::Scheduler() :
@@ -30,6 +31,39 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {
 	is_enabled[threadid]=enabled_status;
 }
 
+enabled_type_t Scheduler::get_enabled(Thread *t) {
+	return is_enabled[id_to_int(t->get_id())];
+}
+
+void Scheduler::update_sleep_set(Node *n) {
+	enabled_type_t *enabled_array=n->get_enabled_array();
+	for(int i=0;i<enabled_len;i++) {
+		if (enabled_array[i]==THREAD_SLEEP_SET) {
+			is_enabled[i]=THREAD_SLEEP_SET;
+		}
+	}
+}
+
+/**
+ * Add a Thread to the sleep set.
+ * @param t The Thread to add
+ */
+void Scheduler::add_sleep(Thread *t)
+{
+	DEBUG("thread %d\n", id_to_int(t->get_id()));
+	set_enabled(t, THREAD_SLEEP_SET);
+}
+
+/**
+ * Remove a Thread from the sleep set.
+ * @param t The Thread to remove
+ */
+void Scheduler::remove_sleep(Thread *t)
+{
+	DEBUG("thread %d\n", id_to_int(t->get_id()));
+	set_enabled(t, THREAD_ENABLED);
+}
+
 /**
  * Add a Thread to the scheduler's ready list.
  * @param t The Thread to add
@@ -86,7 +120,7 @@ Thread * Scheduler::next_thread(Thread *t)
 		int old_curr_thread = curr_thread_index;
 		while(true) {
 			curr_thread_index = (curr_thread_index+1) % enabled_len;
-			if (is_enabled[curr_thread_index]) {
+			if (is_enabled[curr_thread_index]==THREAD_ENABLED) {
 				t = model->get_thread(int_to_id(curr_thread_index));
 				break;
 			}
diff --git a/schedule.h b/schedule.h
index 18936b6..3a54e8c 100644
--- a/schedule.h
+++ b/schedule.h
@@ -10,6 +10,7 @@
 
 /* Forward declaration */
 class Thread;
+class Node;
 
 typedef enum enabled_type {
 	THREAD_DISABLED,
@@ -30,7 +31,10 @@ public:
 	Thread * get_current_thread() const;
 	void print() const;
 	enabled_type_t * get_enabled() { return is_enabled; };
-
+	void remove_sleep(Thread *t);
+	void add_sleep(Thread *t);
+	enabled_type_t get_enabled(Thread *t);
+	void update_sleep_set(Node *n);
 	SNAPSHOTALLOC
 private:
 	/** The list of available Threads that are not currently running */
-- 
2.34.1