X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=8b7201f1b88c4edf98475e0ebeadc7ecd6fd6f32;hb=bbc3405aa23e6eafb3863738c4e203764694e9a4;hp=73d212d0166d2ac3d2fc7368f25afac0333ac491;hpb=12b1a10eeff58161619bafcfd8e288b3e2c76621;p=model-checker.git

diff --git a/model.cc b/model.cc
index 73d212d..8b7201f 100644
--- a/model.cc
+++ b/model.cc
@@ -941,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;
 					}
@@ -1066,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;
 			}
 
@@ -1090,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) &&
@@ -1635,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());
@@ -1739,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);
@@ -1753,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);