From: Brian Demsky <bdemsky@uci.edu>
Date: Sat, 3 Nov 2012 05:14:17 +0000 (-0700)
Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
X-Git-Tag: pldi2013~13^2~7
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=e8e32b7efa96a0b36c1475b58368d002408a7ea7;hp=-c

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

e8e32b7efa96a0b36c1475b58368d002408a7ea7
diff --combined model.cc
index 0fb315e,f67b552..09e6b9d
--- a/model.cc
+++ b/model.cc
@@@ -218,8 -218,7 +218,8 @@@ void ModelChecker::execute_sleep_set() 
  	for(unsigned int i=0;i<get_num_threads();i++) {
  		thread_id_t tid=int_to_id(i);
  		Thread *thr=get_thread(tid);
 -		if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
 +		if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
 +				 thr->get_pending() == NULL ) {
  			thr->set_state(THREAD_RUNNING);
  			scheduler->next_thread(thr);
  			Thread::swap(&system_context, thr);
@@@ -972,7 -971,7 +972,7 @@@ bool ModelChecker::promises_expired() 
  /** @return whether the current partial trace must be a prefix of a
   * feasible trace. */
  bool ModelChecker::isfeasibleprefix() {
 -	return promises->size() == 0 && pending_rel_seqs->size() == 0;
 +	return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
  }
  
  /** @return whether the current partial trace is feasible. */
@@@ -1095,7 -1094,7 +1095,7 @@@ void ModelChecker::check_recency(ModelA
  				ModelAction *act=*rit;
  				bool foundvalue = false;
  				for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
- 					if (act->get_node()->get_read_from_at(i)==write) {
+ 					if (act->get_node()->get_read_from_at(j)==write) {
  						foundvalue = true;
  						break;
  					}