From 8da693d1a0d03aeba127f434c84fcb372314b93a Mon Sep 17 00:00:00 2001 From: Brian Norris 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