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 --cc action.cc
Simple merge

diff --cc model.cc
index 2c27567954f3618c9a94e3e5640955d5b08b1475,8267377faa791a2cfbc85f9027949c7338186635..4f2719f338c8afa9ba05d2f0835fd565bd6dfbd2
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -166,20 -167,19 +170,24 @@@ Thread * ModelChecker::get_next_thread(
                        /* The next node will try to read from a different future value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
+               } else if (nextnode->increment_relseq_break()) {
+                       /* The next node will try to resolve a release sequence differently */
+                       tid = next->get_tid();
+                       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;

diff --cc model.h
Simple merge

diff --cc nodestack.cc
Simple merge

diff --cc nodestack.h
index 147b0048eb9cb00c82bf82c7855c2fe78a6414b8,cb281cad65b1dbf7f60892f9c656ce0061afee84..803d2b8e492c05a98f23a628550dd4f05265e23f
--- 1/nodestack.h
--- 2/nodestack.h
+++ b/nodestack.h
@@@ -90,8 -90,12 +90,13 @@@ 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();
+       bool increment_relseq_break();
+       bool relseq_break_empty();
+ 
        void print();
        void print_may_read_from();
  

diff --cc schedule.cc
index c5e58fe65cb50960db366bd39fb45177ec6fc7db,dd35237b22232df0744e22baadaaceb54ae6affd..ea1d58208ea2b692ed19596c2929a73b254fc998
--- 1/schedule.cc
--- 2/schedule.cc
+++ b/schedule.cc
@@@ -21,47 -20,25 +21,58 @@@ void Scheduler::set_enabled(Thread *t, 
        if (threadid>=enabled_len) {
                enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1));
                memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(enabled_type_t));
-               if (is_enabled != NULL) {
-                       memcpy(new_enabled, is_enabled, enabled_len*sizeof(enabled_type_t));
-                       snapshot_free(is_enabled);
+               if (enabled != NULL) {
+                       memcpy(new_enabled, enabled, enabled_len*sizeof(enabled_type_t));
+                       snapshot_free(enabled);
                }
-               is_enabled=new_enabled;
+               enabled=new_enabled;
                enabled_len=threadid+1;
        }
-       is_enabled[threadid]=enabled_status;
+       enabled[threadid]=enabled_status;
+ }
+ 
+ /**
+  * @brief Check if a Thread is currently enabled
+  * @param t The Thread to check
+  * @return True if the Thread is currently enabled
+  */
+ 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 is_enabled[id_to_int(t->get_id())];
++      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) {
-                       is_enabled[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);
  }
  
  /**
@@@ -120,7 -99,7 +133,7 @@@ Thread * Scheduler::next_thread(Thread 
                int old_curr_thread = curr_thread_index;
                while(true) {
                        curr_thread_index = (curr_thread_index+1) % enabled_len;
-                       if (is_enabled[curr_thread_index]==THREAD_ENABLED) {
 -                      if (enabled[curr_thread_index]) {
++                      if (enabled[curr_thread_index]==THREAD_ENABLED) {
                                t = model->get_thread(int_to_id(curr_thread_index));
                                break;
                        }

diff --cc schedule.h
index 3a54e8cfda9a55c2bcce5af72bc006bcf32a4588,3feddd9025915e9275efc1bf4aca389a1a17844f..72670590dac3151bc9509ca2b5d60f2fe665c210
--- 1/schedule.h
--- 2/schedule.h
+++ b/schedule.h
@@@ -30,11 -29,9 +30,13 @@@ public
        Thread * next_thread(Thread *t);
        Thread * get_current_thread() const;
        void print() const;
-       enabled_type_t * get_enabled() { return is_enabled; };
+       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
  private:
        /** The list of available Threads that are not currently running */