From 8da693d1a0d03aeba127f434c84fcb372314b93a Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 29 May 2012 10:29:59 -0700
Subject: [PATCH] model: thread creation establishes synchronization
First, I add a get_parent_action() wrapper which finds either the last action
in the current thread (get_last_action()) or if NULL, finds the parent
thread-creation action.
Then, using this functionality, I provide the correct 'parent' to the
explore_action() function, which performs the clock-vector creation.
---
model.cc | 18 ++++++++++++++++--
model.h | 1 +
2 files changed, 17 insertions(+), 2 deletions(-)
diff --git a/model.cc b/model.cc
index 142ae3e..274a2d9 100644
--- a/model.cc
+++ b/model.cc
@@ -211,8 +211,14 @@ void ModelChecker::check_current_action(void)
return;
}
- /* TODO: if get_last_action() is NULL, sync with parent thread */
- curr = node_stack->explore_action(curr, get_last_action(curr->get_tid()));
+ curr = node_stack->explore_action(curr, get_parent_action(curr->get_tid()));
+
+ /* Assign 'creation' parent */
+ if (curr->get_type() == THREAD_CREATE) {
+ Thread *th = (Thread *)curr->get_location();
+ th->set_creation(curr);
+ }
+
nextThread = get_next_replay_thread();
currnode = curr->get_node();
@@ -246,6 +252,14 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid)
return (*thrd_last_action)[id_to_int(tid)];
}
+ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
+{
+ ModelAction *parent = get_last_action(tid);
+ if (!parent)
+ parent = get_thread(tid)->get_creation();
+ return parent;
+}
+
void ModelChecker::print_summary(void)
{
printf("\n");
diff --git a/model.h b/model.h
index b59e29c..d89a8a2 100644
--- a/model.h
+++ b/model.h
@@ -58,6 +58,7 @@ private:
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid);
+ ModelAction * get_parent_action(thread_id_t tid);
void print_list(action_list_t *list);
--
2.34.1