merge massive speedup with release sequence support...

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

Conflicts:
	schedule.cc
	schedule.h

diff --git a/action.cc b/action.cc
index 09352da0b0f30f030c5fb423ddd5d60dfdb5dd0c..c1adc2e7bc65cd94d26a4b7cf93ac3482c2b2d1a 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
 
@@ -30,6 +31,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        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 8267377faa791a2cfbc85f9027949c7338186635..4f2719f338c8afa9ba05d2f0835fd565bd6dfbd2 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -154,6 +154,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. */
@@ -173,13 +176,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;
@@ -191,6 +199,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.
@@ -278,7 +320,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.
@@ -303,9 +345,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;
@@ -323,7 +366,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;
@@ -711,7 +753,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)) {
@@ -722,8 +763,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);
@@ -735,7 +779,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();
@@ -797,9 +840,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 68831b867885fe83a7765e2716c8d07cc67f9726..7bc3585d8562eeff369cf307b81751781e381f6b 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 72c8d5cf5e46f7dca4241aa12f26958439ad15c3..3db80e8f6b4f8931ad3a238215c4294c86cd9708 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -267,13 +267,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 cb281cad65b1dbf7f60892f9c656ce0061afee84..803d2b8e492c05a98f23a628550dd4f05265e23f 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 add_relseq_break(const ModelAction *write);
        const ModelAction * get_relseq_break();

diff --git a/schedule.cc b/schedule.cc
index dd35237b22232df0744e22baadaaceb54ae6affd..ea1d58208ea2b692ed19596c2929a73b254fc998 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() :
@@ -38,7 +39,40 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {
 bool Scheduler::is_enabled(Thread *t) const
 {
        int id = id_to_int(t->get_id());
-       return (id >= enabled_len) ? false : (enabled[id] == THREAD_ENABLED);
+       return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED);
+}
+
+enabled_type_t Scheduler::get_enabled(Thread *t) {
+       return 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) {
+                       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);
 }
 
 /**
@@ -99,7 +133,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 (enabled[curr_thread_index]) {
+                       if (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 3feddd9025915e9275efc1bf4aca389a1a17844f..72670590dac3151bc9509ca2b5d60f2fe665c210 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,6 +31,10 @@ public:
        Thread * get_current_thread() const;
        void print() const;
        enabled_type_t * get_enabled() { return enabled; };
+       void remove_sleep(Thread *t);
+       void add_sleep(Thread *t);
+       enabled_type_t get_enabled(Thread *t);
+       void update_sleep_set(Node *n);
        bool is_enabled(Thread *t) const;
 
        SNAPSHOTALLOC