X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=c01122191d0e712750b382f87b9c0edbfecf9aa2;hb=8497408d26002ec1a9d7cfd42458f92f2cdd9864;hp=1598fb9a276343ba3daf59f3beedad6d452115e7;hpb=eb3b6cccf71b9eeee035e2c98566dfa279e402ae;p=model-checker.git

diff --git a/model.cc b/model.cc
index 1598fb9..c011221 100644
--- a/model.cc
+++ b/model.cc
@@ -139,6 +139,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 	ModelAction *next = node_stack->get_next()->get_action();
 
 	if (next == diverge) {
+		if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+			earliest_diverge=diverge;
+
 		Node *nextnode = next->get_node();
 		/* Reached divergence point */
 		if (nextnode->increment_promise()) {
@@ -158,8 +161,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			Node *node = nextnode->get_parent();
 			tid = node->get_next_backtrack();
 			node_stack->pop_restofstack(1);
+			if (diverge==earliest_diverge) {
+				earliest_diverge=node->get_action();
+			}
 		}
 		DEBUG("*** Divergence point ***\n");
+
 		diverge = NULL;
 	} else {
 		tid = next->get_tid();
@@ -181,23 +188,27 @@ bool ModelChecker::next_execution()
 	DBG();
 
 	num_executions++;
+
 	if (isfinalfeasible()) {
 		printf("Earliest divergence point since last feasible execution:\n");
-		earliest_diverge->print();
+		if (earliest_diverge)
+			earliest_diverge->print(false);
+		else
+			printf("(Not set)\n");
 
 		earliest_diverge = NULL;
 		num_feasible_executions++;
 	}
 
+	DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+			pending_acq_rel_seq->size());
+
 	if (isfinalfeasible() || DBG_ENABLED())
 		print_summary();
 
 	if ((diverge = get_next_backtrack()) == NULL)
 		return false;
 
-	if (earliest_diverge == NULL || *diverge < *earliest_diverge)
-		earliest_diverge=diverge;
-
 	if (DBG_ENABLED()) {
 		printf("Next execution will diverge at:\n");
 		diverge->print();
@@ -423,7 +434,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 		action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
 		//activate all the waiting threads
 		for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
-			scheduler->add_thread(get_thread((*rit)->get_tid()));
+			scheduler->wake(get_thread(*rit));
 		}
 		waiters->clear();
 		break;
@@ -468,11 +479,11 @@ bool ModelChecker::process_write(ModelAction *curr)
  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
  *
  * @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated or a thread completed
  */
 bool ModelChecker::process_thread_action(ModelAction *curr)
 {
-	bool synchronized = false;
+	bool updated = false;
 
 	switch (curr->get_type()) {
 	case THREAD_CREATE: {
@@ -489,7 +500,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 			scheduler->sleep(waiting);
 		} else {
 			do_complete_join(curr);
-			synchronized = true;
+			updated = true; /* trigger rel-seq checks */
 		}
 		break;
 	}
@@ -500,9 +511,10 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 			Thread *wake = get_thread(act);
 			scheduler->wake(wake);
 			do_complete_join(act);
-			synchronized = true;
+			updated = true; /* trigger rel-seq checks */
 		}
 		th->complete();
+		updated = true; /* trigger rel-seq checks */
 		break;
 	}
 	case THREAD_START: {
@@ -513,7 +525,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		break;
 	}
 
-	return synchronized;
+	return updated;
 }
 
 /**
@@ -540,6 +552,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		return newcurr;
 	}
 
+	curr->set_seq_number(get_next_seq_num());
+
 	newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
 	if (newcurr) {
 		/* First restore type and order in case of RMW operation */
@@ -612,7 +626,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		/* Make the execution look like we chose to run this action
 		 * much later, when a lock is actually available to release */
 		get_current_thread()->set_pending(curr);
-		remove_thread(get_current_thread());
+		scheduler->sleep(get_current_thread());
 		return get_next_thread(NULL);
 	}
 
@@ -1314,6 +1328,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 		}
 
 		if (updated) {
+			/* Re-check all pending release sequences */
+			work_queue->push_back(CheckRelSeqWorkEntry(NULL));
 			/* Re-check act for mo_graph edges */
 			work_queue->push_back(MOEdgeWorkEntry(act));
 
@@ -1465,6 +1481,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			//Make sure the promise's value matches the write's value
 			ASSERT(promise->get_value() == write->get_value());
 
+			delete(promise);
 			promises->erase(promises->begin() + promise_index);
 			resolved = true;
 		} else