From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 7 Sep 2012 01:56:39 +0000 (-0700)
Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=c5b57f3d98d1d14b4546995a0882753cf71a1c4b

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

check in my stuff...

Conflicts:
	model.cc
	threads.h
---

c5b57f3d98d1d14b4546995a0882753cf71a1c4b
diff --cc model.cc
index 0e2b818c,56723c7d..217d6421
--- a/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) {