From d0d6770dbaf99df616c3c1a142581514e8231c70 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 18 Sep 2012 18:45:17 -0700
Subject: [PATCH] model: THREAD_JOIN synchronizes with THREAD_FINISH

---
 model.cc | 16 ++++++++++++++++
 model.h  |  1 +
 2 files changed, 17 insertions(+)

diff --git a/model.cc b/model.cc
index e41bc4e9..2b295dea 100644
--- 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 b8a48593..b2b312f8 100644
--- 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;
 
-- 
2.34.1