model: note the DPOR addendum
authorBrian Norris <banorris@uci.edu>
Thu, 4 Apr 2013 00:55:49 +0000 (17:55 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 4 Apr 2013 02:29:54 +0000 (19:29 -0700)
To prevent having problems with this in the future.

model.cc

index 6a79ad4..b93653b 100644 (file)
--- 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;