X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=f385e560f085cc9af3aec101207f732a7a3ef8e3;hp=6a79ad4a90f80ff1ee3177511683cd96c67ebb54;hb=e52837077816345a2afa94b42195992a5871824c;hpb=34890ed433f2d30ac5c49342e94d3c5e5f47dbfb

diff --git a/model.cc b/model.cc
index 6a79ad4a..f385e560 100644
--- a/model.cc
+++ b/model.cc
@@ -154,9 +154,6 @@ void ModelChecker::reset_to_initial_state()
 	DEBUG("+++ Resetting to initial state +++\n");
 	node_stack->reset_execution();
 
-	/* Print all model-checker output before rollback */
-	fflush(model_out);
-
 	/**
 	 * FIXME: if we utilize partial rollback, we will need to free only
 	 * those pending actions which were NOT pending before the rollback
@@ -755,6 +752,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
 	Node *node = prev->get_node()->get_parent();
 
+	/* See Dynamic Partial Order Reduction (addendum), POPL '05 */
 	int low_tid, high_tid;
 	if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
 		low_tid = id_to_int(act->get_tid());
@@ -771,6 +769,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 		if (i >= node->get_num_threads())
 			break;
 
+		/* See Dynamic Partial Order Reduction (addendum), POPL '05 */
 		/* Don't backtrack into a point where the thread is disabled or sleeping. */
 		if (node->enabled_status(tid) != THREAD_ENABLED)
 			continue;