From c5e14aa2426f21f8de620cf24ed321447d75c989 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 3 May 2012 23:46:43 -0700 Subject: [PATCH] bugfix - set backtrack events according to an *enabled* thread Previously, I naively set a backtracking point for the thread that performed the conflicting action, whether or not that thread existed at the point to which I am backtracking. Utilize the TreeNode::is_enabled() method, plus thread parent walking, to find the correct thread for the backtracking. Note that this also requires a model checking event for each THREAD_CREATE event. So add this feature. --- libthreads.cc | 2 ++ model.cc | 3 +++ 2 files changed, 5 insertions(+) diff --git a/libthreads.cc b/libthreads.cc index 73a948c..b5760ae 100644 --- a/libthreads.cc +++ b/libthreads.cc @@ -14,6 +14,8 @@ int thrd_create(thrd_t *t, void (*start_routine)(), void *arg) DBG(); ret = model->add_thread(new Thread(t, start_routine, arg)); DEBUG("create thread %d\n", id_to_int(thrd_to_id(*t))); + /* seq_cst is just a 'don't care' parameter */ + model->switch_to_master(new ModelAction(THREAD_CREATE, memory_order_seq_cst, NULL, VALUE_NONE)); return ret; } diff --git a/model.cc b/model.cc index 0084e74..e323825 100644 --- a/model.cc +++ b/model.cc @@ -190,6 +190,9 @@ void ModelChecker::set_backtracking(ModelAction *act) node = prev->get_node(); + while (t && !node->is_enabled(t)) + t = t->get_parent(); + /* Check if this has been explored already */ if (node->hasBeenExplored(t->get_id())) return; -- 2.34.1