merge massive speedup with release sequence support...
authorBrian Demsky <bdemsky@uci.edu>
Mon, 8 Oct 2012 08:21:35 +0000 (01:21 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Mon, 8 Oct 2012 08:21:35 +0000 (01:21 -0700)
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

Conflicts:
schedule.cc
schedule.h

1  2 
action.cc
model.cc
model.h
nodestack.cc
nodestack.h
schedule.cc
schedule.h

diff --cc action.cc
Simple merge
diff --cc 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
@@@ -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
@@@ -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
@@@ -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 */