X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=8b7201f1b88c4edf98475e0ebeadc7ecd6fd6f32;hp=40519e5315a62b12d78d6427a5ab5001236c267f;hb=bbc3405aa23e6eafb3863738c4e203764694e9a4;hpb=1ced3dc2f0a7640ec7f724c477ea87affc697ea9

diff --git a/model.cc b/model.cc
index 40519e5..8b7201f 100644
--- a/model.cc
+++ b/model.cc
@@ -12,6 +12,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "mutex.h"
+#include "threads.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -99,6 +100,12 @@ int ModelChecker::get_num_threads()
 	return priv->next_thread_id;
 }
 
+/** @return The currently executing Thread. */
+Thread * ModelChecker::get_current_thread()
+{
+	return scheduler->get_current_thread();
+}
+
 /** @return a sequence number for a new ModelAction */
 modelclock_t ModelChecker::get_next_seq_num()
 {
@@ -139,6 +146,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 +168,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,6 +195,7 @@ bool ModelChecker::next_execution()
 	DBG();
 
 	num_executions++;
+
 	if (isfinalfeasible()) {
 		printf("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
@@ -192,15 +207,15 @@ bool ModelChecker::next_execution()
 		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();
@@ -426,7 +441,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;
@@ -471,11 +486,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: {
@@ -492,7 +507,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;
 	}
@@ -503,9 +518,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: {
@@ -516,7 +532,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		break;
 	}
 
-	return synchronized;
+	return updated;
 }
 
 /**
@@ -543,6 +559,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 */
@@ -615,7 +633,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);
 	}
 
@@ -923,7 +941,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 					}
 				} else {
 					const ModelAction *prevreadfrom = act->get_reads_from();
-					if (prevreadfrom != NULL && rf != prevreadfrom) {
+					//if the previous read is unresolved, keep going...
+					if (prevreadfrom == NULL)
+						continue;
+
+					if (rf != prevreadfrom) {
 						mo_graph->addEdge(prevreadfrom, rf);
 						added = true;
 					}
@@ -1048,14 +1070,22 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 			ModelAction *act = *rit;
 			if (act == curr) {
 				/*
-				 * If RMW, we already have all relevant edges,
-				 * so just skip to next thread.
-				 * If normal write, we need to look at earlier
-				 * actions, so continue processing list.
+				 * 1) If RMW and it actually read from something, then we
+				 * already have all relevant edges, so just skip to next
+				 * thread.
+				 * 
+				 * 2) If RMW and it didn't read from anything, we should
+				 * whatever edge we can get to speed up convergence.
+				 *
+				 * 3) If normal write, we need to look at earlier actions, so
+				 * continue processing list.
 				 */
-				if (curr->is_rmw())
-					break;
-				else
+				if (curr->is_rmw()) {
+					if (curr->get_reads_from()!=NULL)
+						break;
+					else 
+						continue;
+				} else
 					continue;
 			}
 
@@ -1072,8 +1102,12 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				 */
 				if (act->is_write())
 					mo_graph->addEdge(act, curr);
-				else if (act->is_read() && act->get_reads_from() != NULL)
+				else if (act->is_read()) { 
+					//if previous read accessed a null, just keep going
+					if (act->get_reads_from() == NULL)
+						continue;
 					mo_graph->addEdge(act->get_reads_from(), curr);
+				}
 				added = true;
 				break;
 			} else if (act->is_read() && !act->is_synchronizing(curr) &&
@@ -1317,6 +1351,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));
 
@@ -1468,6 +1504,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
@@ -1614,7 +1651,8 @@ void ModelChecker::dumpGraph(char *filename) {
 		ModelAction *action=*it;
 		if (action->is_read()) {
 			fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
-			fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+			if (action->get_reads_from()!=NULL)
+				fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
 		}
 		if (thread_array[action->get_tid()] != NULL) {
 			fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
@@ -1670,12 +1708,35 @@ void ModelChecker::remove_thread(Thread *t)
 	scheduler->remove_thread(t);
 }
 
+/**
+ * @brief Get a Thread reference by its ID
+ * @param tid The Thread's ID
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(thread_id_t tid)
+{
+	return thread_map->get(id_to_int(tid));
+}
+
+/**
+ * @brief Get a reference to the Thread in which a ModelAction was executed
+ * @param act The ModelAction
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(ModelAction *act)
+{
+	return get_thread(act->get_tid());
+}
+
 /**
  * Switch from a user-context to the "master thread" context (a.k.a. system
  * context). This switch is made with the intention of exploring a particular
  * model-checking action (described by a ModelAction object). Must be called
  * from a user-thread context.
- * @param act The current action that will be explored. Must not be NULL.
+ *
+ * @param act The current action that will be explored. May be NULL only if
+ * trace is exiting via an assertion (see ModelChecker::set_assert and
+ * ModelChecker::has_asserted).
  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
  */
 int ModelChecker::switch_to_master(ModelAction *act)
@@ -1695,7 +1756,7 @@ bool ModelChecker::take_step() {
 	if (has_asserted())
 		return false;
 
-	Thread * curr = thread_current();
+	Thread *curr = thread_current();
 	if (curr) {
 		if (curr->get_state() == THREAD_READY) {
 			ASSERT(priv->current_action);
@@ -1709,22 +1770,22 @@ bool ModelChecker::take_step() {
 			ASSERT(false);
 		}
 	}
-	Thread * next = scheduler->next_thread(priv->nextThread);
+	Thread *next = scheduler->next_thread(priv->nextThread);
 
 	/* Infeasible -> don't take any more steps */
 	if (!isfeasible())
 		return false;
 
-	if (next)
-		next->set_state(THREAD_RUNNING);
 	DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
 
 	/* next == NULL -> don't take any more steps */
 	if (!next)
 		return false;
 
-	if ( next->get_pending() != NULL ) {
-		//restart a pending action
+	next->set_state(THREAD_RUNNING);
+
+	if (next->get_pending() != NULL) {
+		/* restart a pending action */
 		set_current_action(next->get_pending());
 		next->set_pending(NULL);
 		next->set_state(THREAD_READY);