add support for sleep sets...

diff --git a/action.cc b/action.cc
index b4f4e434934cfd0d68adf06ba54bd2b5ada102a0..8dba82f3a8ff7d97967410cfa75b33a84394de98 100644 (file)
--- 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 c3f6372517d591c5016cb91127adf36ae8fadb36..2c27567954f3618c9a94e3e5640955d5b08b1475 100644 (file)
--- 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 d5dc42266769004d542d72f472f6e1029c1a7e5c..d2baaf45afee14661a02c620649e4efdfcf107ee 100644 (file)
--- 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 4cf89500fc1faba0f98714173fbd4eca557edefa..76d167d82a9438e6cd941d114c5a172867ca0780 100644 (file)
--- 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 55deac5beffa2a6a0d3deec210c4246f0b8074db..147b0048eb9cb00c82bf82c7855c2fe78a6414b8 100644 (file)
--- 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 a236bd0cc66644197e178e00d4cc44b0a195f3c2..c5e58fe65cb50960db366bd39fb45177ec6fc7db 100644 (file)
--- 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 18936b612dacbed81e91a949d164e990b5f964b5..3a54e8cfda9a55c2bcce5af72bc006bcf32a4588 100644 (file)
--- 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 */