From: Brian Norris <banorris@uci.edu>
Date: Thu, 4 Apr 2013 00:55:49 +0000 (-0700)
Subject: model: note the DPOR addendum
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=bb9f87c3a725c82882788a9d4baa405ea2aba5d2;ds=sidebyside

model: note the DPOR addendum

To prevent having problems with this in the future.
---

diff --git a/model.cc b/model.cc
index 6a79ad4a..b93653be 100644
--- a/model.cc
+++ b/model.cc
@@ -755,6 +755,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 +772,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;