X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=09e6b9da3150ddc88de4cc4b8ce363725cc493f3;hb=e8e32b7efa96a0b36c1475b58368d002408a7ea7;hp=7181f86977688054159da03d0c3a7921ce23c958;hpb=b5cdd7ee16b73bbfe53040d23994351f85f83785;p=model-checker.git

diff --git a/model.cc b/model.cc
index 7181f86..09e6b9d 100644
--- a/model.cc
+++ b/model.cc
@@ -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);
@@ -383,8 +384,12 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	for(int i = low_tid; i < high_tid; i++) {
 		thread_id_t tid = int_to_id(i);
 
+		/* Make sure this thread can be enabled here. */
+		if (i >= node->get_num_threads())
+			break;
+
 		/* Don't backtrack into a point where the thread is disabled or sleeping. */
-		if (node->get_enabled_array()[i]!=THREAD_ENABLED)
+		if (node->enabled_status(tid)!=THREAD_ENABLED)
 			continue;
 	
 		/* Check if this has been explored already */
@@ -967,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. */
@@ -1090,7 +1095,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
 				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;
 					}
@@ -2021,7 +2026,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
 	while(true) {
 		Node *prevnode=write->get_node()->get_parent();
-		bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+		
+		bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
 		if (write->is_release()&&thread_sleep)
 			return true;
 		if (!write->is_rmw()) {