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

check in my stuff...

Conflicts:
	model.cc
	threads.h

diff --cc model.cc
index 0e2b818cd26487df48b0968484e9533c984a8443,56723c7d5660077c3b1e27d484976d5092388bd7..217d6421ac403e60108ec074c900168bbce67888
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -9,6 -9,6 +9,7 @@@
  #include "clockvector.h"
  #include "cyclegraph.h"
  #include "promise.h"
++#include "datarace.h"
  
  #define INITIAL_THREAD_ID     0
  
@@@ -36,7 -36,7 +37,8 @@@ ModelChecker::ModelChecker(struct model
        node_stack(new NodeStack()),
        next_backtrack(NULL),
        mo_graph(new CycleGraph()),
--      failed_promise(false)
++      failed_promise(false),
++      asserted(false)
  {
  }
  
@@@ -77,6 -77,6 +79,7 @@@ void ModelChecker::reset_to_initial_sta
        nextThread = NULL;
        next_backtrack = NULL;
        failed_promise = false;
++      reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
  }
  
@@@ -326,7 -339,7 +342,7 @@@ Thread * ModelChecker::check_current_ac
                }
        } else if (curr->is_write()) {
                if (w_modification_order(curr))
--                      updated = true;;
++                      updated = true;
                if (resolve_promises(curr))
                        updated = true;
        }
@@@ -357,12 -370,6 +373,13 @@@
                return get_next_replay_thread();
  }
  
 +/** @returns whether the current partial trace must be a prefix of a
 + * feasible trace. */
 +
 +bool ModelChecker::isfeasibleprefix() {
++      return promises->size()==0;
 +}
 +
  /** @returns whether the current partial trace is feasible. */
  bool ModelChecker::isfeasible() {
        return !mo_graph->checkForCycles() && !failed_promise;
@@@ -693,6 -700,6 +710,11 @@@ bool ModelChecker::resolve_release_sequ
                        it++;
        }
  
++      // If we resolved promises or data races, see if we have realized a data race.
++      if (checkDataRaces()) {
++              model->set_assert();
++      }
++
        return updated;
  }
  
@@@ -784,6 -791,6 +806,7 @@@ bool ModelChecker::resolve_promises(Mod
                } else
                        promise_index++;
        }
++
        return resolved;
  }
  
@@@ -977,6 -973,6 +989,9 @@@ int ModelChecker::switch_to_master(Mode
  bool ModelChecker::take_step() {
        Thread *curr, *next;
  
++      if (has_asserted())
++              return false;
++
        curr = thread_current();
        if (curr) {
                if (curr->get_state() == THREAD_READY) {