Merge branch 'master' into brian

diff --combined action.cc
index c96949bc906cc02a9ca3cb50af761a92feda94c7,d9aae2d4958253977e9f0256fb87076174e94a67..39b0f7f6d4847207f0dc2a18da5b0edeffa5776a
--- 1/action.cc
--- 2/action.cc
+++ b/action.cc
@@@ -10,7 -10,6 +10,7 @@@ ModelAction::ModelAction(action_type_t 
        order(order),
        location(loc),
        value(value),
 +      reads_from(NULL),
        cv(NULL)
  {
        Thread *t = thread_current();
@@@ -102,7 -101,7 +102,7 @@@ bool ModelAction::is_synchronizing(cons
        // Different locations commute
        if (!same_var(act))
                return false;
-       
+ 
        // Explore interleavings of seqcst writes to guarantee total order
        // of seq_cst operations that don't commute
        if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst())
@@@ -133,7 -132,6 +133,7 @@@ void ModelAction::read_from(const Model
        ASSERT(cv);
        if (act->is_release() && this->is_acquire())
                cv->merge(act->cv);
 +      reads_from = act;
        value = act->value;
  }
  
@@@ -155,6 -153,9 +155,9 @@@ void ModelAction::print(void) cons
        case THREAD_CREATE:
                type_str = "thread create";
                break;
+       case THREAD_START:
+               type_str = "thread start";
+               break;
        case THREAD_YIELD:
                type_str = "thread yield";
                break;
@@@ -177,10 -178,8 +180,10 @@@
                type_str = "unknown type";
        }
  
 -      printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %d",
 +      printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %-4d",
                        seq_number, id_to_int(tid), type_str, order, location, value);
 +      if (reads_from)
 +              printf(" Rf: %d", reads_from->get_seq_number());
        if (cv) {
                printf("\t");
                cv->print();

diff --combined action.h
index 731c3192f747b083bc0f26e6b0961c432bc90514,3e4480419c03941413307ebba6a6e27a77372109..30c8a35b80ed7681ce74bc5388c0667b9b4e4fec
--- 1/action.h
--- 2/action.h
+++ b/action.h
@@@ -19,6 -19,7 +19,7 @@@
   * ModelAction */
  typedef enum action_type {
        THREAD_CREATE,        /**< A thread creation action */
+       THREAD_START,         /**< First action in each thread */
        THREAD_YIELD,         /**< A thread yield action */
        THREAD_JOIN,          /**< A thread join action */
        ATOMIC_READ,          /**< An atomic read action */
@@@ -47,10 -48,10 +48,10 @@@ public
        void * get_location() const { return location; }
        modelclock_t get_seq_number() const { return seq_number; }
        int get_value() const { return value; }
 +      const ModelAction * get_reads_from() const { return reads_from; }
  
        Node * get_node() const { return node; }
        void set_node(Node *n) { node = n; }
 -      void set_value(int val) { value = val; }
  
        bool is_read() const;
        bool is_write() const;
@@@ -90,18 -91,15 +91,18 @@@ private
  
        /** The thread id that performed this action. */
        thread_id_t tid;
-       
+ 
        /** The value read or written (if RMW, then the value written). This
         * should probably be something longer. */
        int value;
  
 +      /** The action that this action reads from. Only valid for reads */
 +      const ModelAction *reads_from;
 +
        /** A back reference to a Node in NodeStack, if this ModelAction is
         * saved on the NodeStack. */
        Node *node;
-       
+ 
        modelclock_t seq_number;
  
        /** The clock vector stored with this action; only needed if this

diff --combined clockvector.cc
index 88ea6fdfcf7cc73a8b99239e9128180883ca55bb,162a7c2550db61c3845885349a01b76e6fd84838..190f9216a92b61ad68df0990775d4c978aaa53f9
--- 1/clockvector.cc
--- 2/clockvector.cc
+++ b/clockvector.cc
@@@ -34,11 -34,11 +34,11 @@@ ClockVector::~ClockVector(
  }
  
  /**
 - * Merge a clock vector into this vector, using a pairwise vector. The
 + * Merge a clock vector into this vector, using a pairwise comparison. The
   * resulting vector length will be the maximum length of the two being merged.
   * @param cv is the ClockVector being merged into this vector.
   */
 -void ClockVector::merge(ClockVector *cv)
 +void ClockVector::merge(const ClockVector *cv)
  {
        modelclock_t *clk = clock;
        bool resize = false;
@@@ -84,7 -84,7 +84,7 @@@ bool ClockVector::synchronized_since(co
        return false;
  }
  
- /** 
+ /**
   * Gets the clock corresponding to a given thread id from the clock
   * vector. */
  

diff --combined main.cc
index 3dff4f424ce2a2b36aa3c1fa7fc8819f30c89af3,19f12f182494685d718a963b23ee01d3ef3ffcb0..c9ac1d0663206feccb6d05d43803689e7214574e
--- 1/main.cc
--- 2/main.cc
+++ b/main.cc
@@@ -6,6 -6,8 +6,8 @@@
  #include "common.h"
  #include "threads.h"
  
+ #include "datarace.h"
+ 
  /* global "model" object */
  #include "model.h"
  #include "snapshot-interface.h"
@@@ -51,10 -53,13 +53,13 @@@ static void thread_wait_finish(void) 
  
  /** The real_main function contains the main model checking loop. */
  
 -void real_main() {
 +static void real_main() {
        thrd_t user_thread;
        ucontext_t main_context;
  
+       //Initialize race detector
+       initRaceDetector();
+ 
        //Create the singleton SnapshotStack object
        snapshotObject = new SnapshotStack();
  

diff --combined model.cc
index 07c81b9eed2108a32df8c50b87fb18c38f355d21,cde6213ada34c0b3c6a9a5328474ddcf9371a726..d80d1d27be741c749d9f94db4e8c5c9f8c28e6d4
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -272,19 -272,6 +272,19 @@@ void ModelChecker::check_current_action
        set_backtracking(curr);
  
        add_action_to_lists(curr);
 +
 +      /* Assign reads_from values */
 +      /* TODO: perform release/acquire synchronization here; include
 +       * reads_from as ModelAction member? */
 +      Thread *th = get_thread(curr->get_tid());
 +      int value = VALUE_NONE;
 +      if (curr->is_read()) {
 +              const ModelAction *reads_from = curr->get_node()->get_next_read_from();
 +              value = reads_from->get_value();
 +              /* Assign reads_from, perform release/acquire synchronization */
 +              curr->read_from(reads_from);
 +      }
 +      th->set_return_value(value);
  }
  
  /**
@@@ -296,14 -283,17 +296,17 @@@
   */
  void ModelChecker::add_action_to_lists(ModelAction *act)
  {
+       int tid = id_to_int(act->get_tid());
        action_trace->push_back(act);
  
        std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
-       if (id_to_int(act->get_tid()) >= (int)vec->size())
+       if (tid >= (int)vec->size())
                vec->resize(next_thread_id);
-       (*vec)[id_to_int(act->get_tid())].push_back(act);
+       (*vec)[tid].push_back(act);
  
-       (*thrd_last_action)[id_to_int(act->get_tid())] = act;
+       if ((int)thrd_last_action->size() <= tid)
+               thrd_last_action->resize(get_num_threads());
+       (*thrd_last_action)[tid] = act;
  }
  
  ModelAction * ModelChecker::get_last_action(thread_id_t tid)
@@@ -322,6 -312,10 +325,10 @@@ ModelAction * ModelChecker::get_parent_
        return parent;
  }
  
+ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
+       return get_parent_action(tid)->get_cv();
+ }
+ 
  /**
   * Build up an initial set of all past writes that this 'read' action may read
   * from. This set is determined by the clock vector's "happens before"