X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=152e36ec2f296fc9f467b890e2e89d6ada3504ee;hp=fab1a5994feb96e6ee22c59e941b7fc9550ff041;hb=c2d0d0dd1f069749e1ee19e5203af048e0b26f1c;hpb=5fa2efec1354b2781ff0b29460ec8e9b8fa75991

diff --git a/model.cc b/model.cc
index fab1a59..152e36e 100644
--- a/model.cc
+++ b/model.cc
@@ -282,6 +282,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 				earliest_diverge = prevnode->get_action();
 			}
 		}
+		/* Start the round robin scheduler from this thread id */
+		scheduler->set_scheduler_thread(tid);
 		/* The correct sleep set is in the parent node. */
 		execute_sleep_set();
 
@@ -313,14 +315,41 @@ void ModelChecker::execute_sleep_set()
 	}
 }
 
+/**
+ * @brief Should the current action wake up a given thread?
+ *
+ * @param curr The current action
+ * @param thread The thread that we might wake up
+ * @return True, if we should wake up the sleeping thread; false otherwise
+ */
+bool ModelChecker::should_wake_up(const ModelAction *curr, const Thread *thread) const
+{
+	const ModelAction *asleep = thread->get_pending();
+	/* Don't allow partial RMW to wake anyone up */
+	if (curr->is_rmwr())
+		return false;
+	/* Synchronizing actions may have been backtracked */
+	if (asleep->could_synchronize_with(curr))
+		return true;
+	/* All acquire/release fences and fence-acquire/store-release */
+	if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
+		return true;
+	/* Fence-release + store can awake load-acquire on the same location */
+	if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
+		ModelAction *fence_release = get_last_fence_release(curr->get_tid());
+		if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
+			return true;
+	}
+	return false;
+}
+
 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
 {
 	for (unsigned int i = 0; i < get_num_threads(); i++) {
 		Thread *thr = get_thread(int_to_id(i));
 		if (scheduler->is_sleep_set(thr)) {
-			ModelAction *pending_act = thr->get_pending();
-			if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
-				//Remove this thread from sleep set
+			if (should_wake_up(curr, thr))
+				/* Remove this thread from sleep set */
 				scheduler->remove_sleep(thr);
 		}
 	}
@@ -545,6 +574,18 @@ bool ModelChecker::next_execution()
 	return true;
 }
 
+/**
+ * @brief Find the last fence-related backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking, as affected by fence
+ * operations. This includes pairs of potentially-synchronizing actions which
+ * occur due to fence-acquire or fence-release, and hence should be explored in
+ * the opposite execution order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act due to fences
+ */
 ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
 {
 	/* Only perform release/acquire fence backtracking for stores */
@@ -560,16 +601,22 @@ ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
 	if (!last_release)
 		return NULL;
 
-	std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
-	std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
-	bool found_acquire_fences = false;
+	/* Skip past the release */
+	action_list_t *list = action_trace;
+	action_list_t::reverse_iterator rit;
+	for (rit = list->rbegin(); rit != list->rend(); rit++)
+		if (*rit == last_release)
+			break;
+	ASSERT(rit != list->rend());
+
 	/* Find a prior:
 	 *   load-acquire
 	 * or
 	 *   load --sb-> fence-acquire */
-	action_list_t *list = action_trace;
-	action_list_t::reverse_iterator rit;
-	for (rit = list->rbegin(); rit != list->rend(); rit++) {
+	std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
+	std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
+	bool found_acquire_fences = false;
+	for ( ; rit != list->rend(); rit++) {
 		ModelAction *prev = *rit;
 		if (act->same_thread(prev))
 			continue;
@@ -600,6 +647,17 @@ ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
 	return latest_backtrack;
 }
 
+/**
+ * @brief Find the last backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking. This primary includes pairs of
+ * synchronizing actions which should be explored in the opposite execution
+ * order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act
+ */
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act) const
 {
 	switch (act->get_type()) {
@@ -1055,7 +1113,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 	case THREAD_CREATE: {
 		thrd_t *thrd = (thrd_t *)curr->get_location();
 		struct thread_params *params = (struct thread_params *)curr->get_value();
-		Thread *th = new Thread(thrd, params->func, params->arg);
+		Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr));
 		add_thread(th);
 		th->set_creation(curr);
 		/* Promises can be satisfied by children */
@@ -1269,6 +1327,30 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 	return false;
 }
 
+/**
+ * Check promises and eliminate potentially-satisfying threads when a thread is
+ * blocked (e.g., join, lock). A thread which is waiting on another thread can
+ * no longer satisfy a promise generated from that thread.
+ *
+ * @param blocker The thread on which a thread is waiting
+ * @param waiting The waiting thread
+ */
+void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
+{
+	for (unsigned int i = 0; i < promises->size(); i++) {
+		Promise *promise = (*promises)[i];
+		ModelAction *reader = promise->get_action();
+		if (reader->get_tid() != blocker->get_id())
+			continue;
+		if (!promise->thread_is_available(waiting->get_id()))
+			continue;
+		if (promise->eliminate_thread(waiting->get_id())) {
+			/* Promise has failed */
+			priv->failed_promise = true;
+		}
+	}
+}
+
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -1292,6 +1374,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 		Thread *blocking = (Thread *)curr->get_location();
 		if (!blocking->is_complete()) {
 			blocking->push_wait_list(curr);
+			thread_blocking_check_promises(blocking, get_thread(curr));
 			return false;
 		}
 	}
@@ -1337,7 +1420,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 
 	/* Build may_read_from set for newly-created actions */
 	if (newly_explored && curr->is_read())
-		build_reads_from_past(curr);
+		build_may_read_from(curr);
 
 	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
@@ -1682,13 +1765,13 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 						added = mo_graph->addEdge(act, rf) || added;
 					}
 				} else {
-					const ModelAction *prevreadfrom = act->get_reads_from();
-					//if the previous read is unresolved, keep going...
-					if (prevreadfrom == NULL)
-						continue;
-
-					if (!prevreadfrom->equals(rf)) {
-						added = mo_graph->addEdge(prevreadfrom, rf) || added;
+					const ModelAction *prevrf = act->get_reads_from();
+					const Promise *prevrf_promise = act->get_reads_from_promise();
+					if (prevrf) {
+						if (!prevrf->equals(rf))
+							added = mo_graph->addEdge(prevrf, rf) || added;
+					} else if (!prevrf_promise->equals(rf)) {
+						added = mo_graph->addEdge(prevrf_promise, rf) || added;
 					}
 				}
 				break;
@@ -2364,7 +2447,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			read_from(read, write);
 			//Make sure the promise's value matches the write's value
 			ASSERT(promise->is_compatible(write));
-			mo_graph->resolvePromise(read, write, &mustResolve);
+			mo_graph->resolvePromise(promise, write, &mustResolve);
 
 			resolved.push_back(promise);
 			promises->erase(promises->begin() + promise_index);
@@ -2404,11 +2487,10 @@ void ModelChecker::compute_promises(ModelAction *curr)
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
 		const ModelAction *act = promise->get_action();
+		ASSERT(act->is_read());
 		if (!act->happens_before(curr) &&
-				act->is_read() &&
 				!act->could_synchronize_with(curr) &&
-				!act->same_thread(curr) &&
-				act->get_location() == curr->get_location() &&
+				promise->is_compatible(curr) &&
 				promise->get_value() == curr->get_value()) {
 			curr->get_node()->set_promise(i, act->is_rmw());
 		}
@@ -2512,12 +2594,12 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
 
 /**
  * Build up an initial set of all past writes that this 'read' action may read
- * from. This set is determined by the clock vector's "happens before"
- * relationship.
+ * from, as well as any previously-observed future values that must still be valid.
+ *
  * @param curr is the current ModelAction that we are exploring; it must be a
  * 'read' operation.
  */
-void ModelChecker::build_reads_from_past(ModelAction *curr)
+void ModelChecker::build_may_read_from(ModelAction *curr)
 {
 	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
@@ -2562,8 +2644,25 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 				break;
 		}
 	}
+
+	/* Inherit existing, promised future values */
+	for (i = 0; i < promises->size(); i++) {
+		const Promise *promise = (*promises)[i];
+		const ModelAction *promise_read = promise->get_action();
+		if (promise_read->same_var(curr)) {
+			/* Only add feasible future-values */
+			mo_graph->startChanges();
+			r_modification_order(curr, promise);
+			if (!is_infeasible()) {
+				const struct future_value fv = promise->get_fv();
+				curr->get_node()->add_future_value(fv);
+			}
+			mo_graph->rollbackChanges();
+		}
+	}
+
 	/* We may find no valid may-read-from only if the execution is doomed */
-	if (!curr->get_node()->get_read_from_size()) {
+	if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) {
 		priv->no_valid_reads = true;
 		set_assert();
 	}
@@ -2815,7 +2914,7 @@ void ModelChecker::run()
 {
 	do {
 		thrd_t user_thread;
-		Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
+		Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL, NULL);
 		add_thread(t);
 
 		do {