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

diff --git a/model.cc b/model.cc
index e394865e26c01d75b05853a55a4b2b7a23c3e853..a96a79c851ee83b5624df3bdafda7487802bf5b1 100644 (file)
--- 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 01dd35b03752504dc9416543f38588018297adf6..d6c033725dedf36bed645f5615f19d45444b2f07 100644 (file)
--- 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 167d6940d37eb20bbac1ad3ccf441661d1a9ed6f..a850478e95391a5eecf1ca26ee12c47e4ab4dfcb 100644 (file)
--- 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 da6d469fdfe81498e9078423a14eb6310a0ad9e3..f68cb528a16b846a2f2653ecd3336b6ca496fee8 100644 (file)
--- 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) {