From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 10 Oct 2012 21:33:30 +0000 (-0700)
Subject: make scheduler choose fair schedules when threads with priority are sleeping...
X-Git-Tag: pldi2013~58^2
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=1b793f0683aff025afe2e19519572e3599575a19;hp=1645d16c883f765168a26892f07d003963d5b68c

make scheduler choose fair schedules when threads with priority are sleeping...
---

diff --git a/model.cc b/model.cc
index e394865..a96a79c 100644
--- a/model.cc
+++ b/model.cc
@@ -116,6 +116,10 @@ modelclock_t ModelChecker::get_next_seq_num()
 	return ++priv->used_sequence_numbers;
 }
 
+Node * ModelChecker::get_curr_node() {
+	return node_stack->get_head();
+}
+
 /**
  * @brief Choose the next thread to execute.
  *
diff --git a/model.h b/model.h
index 01dd35b..d6c0337 100644
--- a/model.h
+++ b/model.h
@@ -112,6 +112,7 @@ public:
 
 	const model_params params;
 	Scheduler * get_scheduler() { return scheduler;}
+	Node * get_curr_node();
 
 	MEMALLOC
 private:
diff --git a/nodestack.cc b/nodestack.cc
index 167d694..a850478 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -49,7 +49,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 				if (prevfi) {
 					*fi=*prevfi;
 				}
-				if (parent->enabled_array[i]==THREAD_ENABLED) {
+				if (parent->is_enabled(i)) {
 					fi->enabled_count++;
 				}
 				if (i==currtid) {
@@ -58,7 +58,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 				}
 				//Do window processing
 				if (prevfairness != NULL) {
-					if (prevfairness -> parent->enabled_array[i] == THREAD_ENABLED)
+					if (prevfairness -> parent->is_enabled(i))
 						fi->enabled_count--;
 					if (i==prevtid) {
 						fi->turns--;
diff --git a/schedule.cc b/schedule.cc
index da6d469..f68cb52 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -131,10 +131,24 @@ Thread * Scheduler::next_thread(Thread *t)
 {
 	if ( t == NULL ) {
 		int old_curr_thread = curr_thread_index;
+		bool have_enabled_thread_with_priority=false;
+		Node *n=model->get_curr_node();
+
+		for(int i=0;i<enabled_len;i++) {
+			thread_id_t tid=int_to_id(i);
+			if (n->has_priority(tid)) {
+				//Have a thread with priority
+				if (enabled[i]!=THREAD_DISABLED)
+					have_enabled_thread_with_priority=true;
+			}
+		}
+
 		while(true) {
 			curr_thread_index = (curr_thread_index+1) % enabled_len;
-			if (enabled[curr_thread_index]==THREAD_ENABLED) {
-				t = model->get_thread(int_to_id(curr_thread_index));
+			thread_id_t curr_tid=int_to_id(curr_thread_index);
+			if (enabled[curr_thread_index]==THREAD_ENABLED&&
+					(!have_enabled_thread_with_priority||n->has_priority(curr_tid))) {
+				t = model->get_thread(int_to_id(curr_tid));
 				break;
 			}
 			if (curr_thread_index == old_curr_thread) {