From: Brian Norris <banorris@uci.edu>
Date: Fri, 4 May 2012 06:46:43 +0000 (-0700)
Subject: bugfix - set backtrack events according to an *enabled* thread
X-Git-Tag: pldi2013~456
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c5e14aa2426f21f8de620cf24ed321447d75c989;p=model-checker.git

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.
---

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;