X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=5753c5c4e016e2a6b7433aeee60706e777505860;hb=1732a51f04b471f5019377c5860672fc3ada0088;hp=02f290d0a4e29efe8954eaf56f1075955182e9ea;hpb=9c42c31b487bf7319dba4d43e417e29420306977;p=model-checker.git

diff --git a/model.cc b/model.cc
index 02f290d..5753c5c 100644
--- a/model.cc
+++ b/model.cc
@@ -12,7 +12,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "mutex.h"
-#include "threads.h"
+#include "threads-model.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -557,26 +557,17 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		break;
 	}
 	case THREAD_JOIN: {
-		Thread *waiting, *blocking;
-		waiting = get_thread(curr);
-		blocking = (Thread *)curr->get_location();
-		if (!blocking->is_complete()) {
-			blocking->push_wait_list(curr);
-			scheduler->sleep(waiting);
-		} else {
-			do_complete_join(curr);
-			updated = true; /* trigger rel-seq checks */
-		}
+		Thread *blocking = (Thread *)curr->get_location();
+		ModelAction *act = get_last_action(blocking->get_id());
+		curr->synchronize_with(act);
+		updated = true; /* trigger rel-seq checks */
 		break;
 	}
 	case THREAD_FINISH: {
 		Thread *th = get_thread(curr);
 		while (!th->wait_list_empty()) {
 			ModelAction *act = th->pop_wait_list();
-			Thread *wake = get_thread(act);
-			scheduler->wake(wake);
-			do_complete_join(act);
-			updated = true; /* trigger rel-seq checks */
+			scheduler->wake(get_thread(act));
 		}
 		th->complete();
 		updated = true; /* trigger rel-seq checks */
@@ -721,9 +712,12 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 }
 
 /**
- * This method checks whether a model action is enabled at the given point.
- * At this point, it checks whether a lock operation would be successful at this point.
- * If not, it puts the thread in a waiter list.
+ * @brief Check whether a model action is enabled.
+ *
+ * Checks whether a lock or join operation would be successful (i.e., is the
+ * lock already locked, or is the joined thread already complete). If not, put
+ * the action in a waiter list.
+ *
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
  */
@@ -736,6 +730,12 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 			lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
 			return false;
 		}
+	} else if (curr->get_type() == THREAD_JOIN) {
+		Thread *blocking = (Thread *)curr->get_location();
+		if (!blocking->is_complete()) {
+			blocking->push_wait_list(curr);
+			return false;
+		}
 	}
 
 	return true;
@@ -760,7 +760,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	if (!check_action_enabled(curr)) {
 		/* Make the execution look like we chose to run this action
-		 * much later, when a lock is actually available to release */
+		 * much later, when a lock/join can succeed */
 		get_current_thread()->set_pending(curr);
 		scheduler->sleep(get_current_thread());
 		return get_next_thread(NULL);
@@ -847,19 +847,6 @@ 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();
@@ -1792,6 +1779,11 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
 			//do we have a pwrite for the promise, if not, set it
 			if (promise->get_write() == NULL ) {
 				promise->set_write(write);
+				//The pwrite cannot happen before the promise
+				if (write->happens_before(act) && (write != act)) {
+					failed_promise = true;
+					return;
+				}
 			}
 			if (mo_graph->checkPromise(write, promise)) {
 				failed_promise = true;