X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=c01122191d0e712750b382f87b9c0edbfecf9aa2;hb=8497408d26002ec1a9d7cfd42458f92f2cdd9864;hp=e3d26d3261968ca4b4eefd3fd593767045b0687b;hpb=a7472bf7d514d8c53b22eb64bc552f593c79d506;p=model-checker.git

diff --git a/model.cc b/model.cc
index e3d26d3..c011221 100644
--- a/model.cc
+++ b/model.cc
@@ -188,6 +188,7 @@ bool ModelChecker::next_execution()
 	DBG();
 
 	num_executions++;
+
 	if (isfinalfeasible()) {
 		printf("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
@@ -199,6 +200,9 @@ bool ModelChecker::next_execution()
 		num_feasible_executions++;
 	}
 
+	DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+			pending_acq_rel_seq->size());
+
 	if (isfinalfeasible() || DBG_ENABLED())
 		print_summary();
 
@@ -488,17 +492,26 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 		break;
 	}
 	case THREAD_JOIN: {
-		Thread *blocking = (Thread *)curr->get_location();
-		ModelAction *act = get_last_action(blocking->get_id());
-		curr->synchronize_with(act);
-		updated = true; /* trigger rel-seq checks */
+		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 */
+		}
 		break;
 	}
 	case THREAD_FINISH: {
 		Thread *th = get_thread(curr);
 		while (!th->wait_list_empty()) {
 			ModelAction *act = th->pop_wait_list();
-			scheduler->wake(get_thread(act));
+			Thread *wake = get_thread(act);
+			scheduler->wake(wake);
+			do_complete_join(act);
+			updated = true; /* trigger rel-seq checks */
 		}
 		th->complete();
 		updated = true; /* trigger rel-seq checks */
@@ -571,12 +584,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 }
 
 /**
- * @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.
- *
+ * 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.
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
  */
@@ -589,12 +599,6 @@ 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;
@@ -620,7 +624,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/join can succeed */
+		 * much later, when a lock is actually available to release */
 		get_current_thread()->set_pending(curr);
 		scheduler->sleep(get_current_thread());
 		return get_next_thread(NULL);
@@ -704,6 +708,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();
@@ -1311,6 +1328,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 		}
 
 		if (updated) {
+			/* Re-check all pending release sequences */
+			work_queue->push_back(CheckRelSeqWorkEntry(NULL));
 			/* Re-check act for mo_graph edges */
 			work_queue->push_back(MOEdgeWorkEntry(act));
 
@@ -1462,6 +1481,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			//Make sure the promise's value matches the write's value
 			ASSERT(promise->get_value() == write->get_value());
 
+			delete(promise);
 			promises->erase(promises->begin() + promise_index);
 			resolved = true;
 		} else