model: THREAD_JOIN synchronizes with THREAD_FINISH

diff --git a/model.cc b/model.cc
index e41bc4e926f39c42487fd833bfd7e6c57d8a0baf..2b295dea1b24d631ce2a0da7942aeed734c8fc46 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -423,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;
        }
@@ -432,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;
@@ -498,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();

diff --git a/model.h b/model.h
index b8a485931882f119ff5b70140c63f213fb79658f..b2b312f890328e5606887e73a62018eced76ba87 100644 (file)
--- a/model.h
+++ b/model.h
@@ -139,6 +139,7 @@ private:
        bool release_seq_head(const ModelAction *rf,
                        std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
+       void do_complete_join(ModelAction *join);
 
        ModelAction *diverge;