X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=ae3788945c7756881178b1657bb215cf5a71901a;hb=6df4a86031c4831b581e39b093c5fad128bda582;hp=8f0b3ce443c4bf9d18eedbf524cd2d6e3c7b91fe;hpb=a01fa7fb82f22ef8d4787fd5d3ad44598a44f924;p=model-checker.git

diff --git a/model.cc b/model.cc
index 8f0b3ce..ae37889 100644
--- a/model.cc
+++ b/model.cc
@@ -313,14 +313,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);
 		}
 	}
@@ -1366,7 +1393,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));
@@ -2541,12 +2568,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;
@@ -2591,8 +2618,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();
 	}