model: THREAD_JOIN synchronizes with THREAD_FINISH

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index a13ccb7d0b7114aaa1a20adbeca5d1eb6927dbc9..2b295dea1b24d631ce2a0da7942aeed734c8fc46 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -333,6 +333,17 @@ bool ModelChecker::process_write(ModelAction *curr)
        return updated_mod_order || updated_promises;
 }
 
+/**
+ * Initialize the current action by performing one or more of the following
+ * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
+ * in the NodeStack, manipulating backtracking sets, allocating and
+ * initializing clock vectors, and computing the promises to fulfill.
+ *
+ * @param curr The current action, as passed from the user context; may be
+ * freed/invalidated after the execution of this function
+ * @return The current action, as processed by the ModelChecker. Is only the
+ * same as the parameter @a curr if this is a newly-explored action.
+ */
 ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 {
        ModelAction *newcurr;
@@ -389,6 +400,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
        ModelAction *newcurr = initialize_curr_action(curr);
 
+       /* Add the action to lists before any other model-checking tasks */
+       if (!second_part_of_rmw)
+               add_action_to_lists(newcurr);
+
        /* Build may_read_from set for newly-created actions */
        if (curr == newcurr && curr->is_read())
                build_reads_from_past(curr);
@@ -408,6 +423,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                if (!blocking->is_complete()) {
                        blocking->push_wait_list(curr);
                        scheduler->sleep(waiting);
+               } else {
+                       do_complete_join(curr);
                }
                break;
        }
@@ -417,6 +434,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        ModelAction *act = th->pop_wait_list();
                        Thread *wake = get_thread(act);
                        scheduler->wake(wake);
+                       do_complete_join(act);
                }
                th->complete();
                break;
@@ -429,10 +447,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                break;
        }
 
-       /* Add current action to lists before work_queue loop */
-       if (!second_part_of_rmw)
-               add_action_to_lists(curr);
-
        work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
 
        while (!work_queue.empty()) {
@@ -487,6 +501,19 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        return get_next_thread(curr);
 }
 
+/**
+ * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
+ * operation from the Thread it is joining with. Must be called after the
+ * completion of the Thread in question.
+ * @param join The THREAD_JOIN action
+ */
+void ModelChecker::do_complete_join(ModelAction *join)
+{
+       Thread *blocking = (Thread *)join->get_location();
+       ModelAction *act = get_last_action(blocking->get_id());
+       join->synchronize_with(act);
+}
+
 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();