From bb9f87c3a725c82882788a9d4baa405ea2aba5d2 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 3 Apr 2013 17:55:49 -0700 Subject: [PATCH] model: note the DPOR addendum To prevent having problems with this in the future. --- model.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/model.cc b/model.cc index 6a79ad4..b93653b 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; -- 2.34.1