From: Brian Norris <banorris@uci.edu>
Date: Wed, 19 Sep 2012 01:45:17 +0000 (-0700)
Subject: model: THREAD_JOIN synchronizes with THREAD_FINISH
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d0d6770dbaf99df616c3c1a142581514e8231c70;p=cdsspec-compiler.git

model: THREAD_JOIN synchronizes with THREAD_FINISH
---

diff --git a/model.cc b/model.cc
index e41bc4e..2b295de 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 b8a4859..b2b312f 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;