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.

diff --git a/model.cc b/model.cc
index 142ae3efdfab1bf0812350a5fc89d37ea45c21b9..274a2d928102f9d2348114e5085f4781f69fe0b6 100644 (file)
--- 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 b59e29cea19b660935824eca736178183910c735..d89a8a2b123b1743c58f3c5d7c883c87263b45b9 100644 (file)
--- 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);