X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=execution.cc;h=3a630d777f060cb22598858278044d6e140cfed3;hp=53aa5212f0b017622d0c284f1cbc765e0620fddd;hb=6014243b7130f34b7ffd1098da225b0b8de5c328;hpb=e79a7cd8e9c85d37a5d5c2a81ca14b1017b1b305

diff --git a/execution.cc b/execution.cc
index 53aa521..3a630d7 100644
--- a/execution.cc
+++ b/execution.cc
@@ -30,6 +30,7 @@ struct model_snapshot_members {
 		next_backtrack(NULL),
 		bugs(),
 		failed_promise(false),
+		hard_failed_promise(false),
 		too_many_reads(false),
 		no_valid_reads(false),
 		bad_synchronization(false),
@@ -47,6 +48,7 @@ struct model_snapshot_members {
 	ModelAction *next_backtrack;
 	SnapVector<bug_message *> bugs;
 	bool failed_promise;
+	bool hard_failed_promise;
 	bool too_many_reads;
 	bool no_valid_reads;
 	/** @brief Incorrectly-ordered synchronization was made */
@@ -1375,7 +1377,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 	char *ptr = buf;
 	if (mo_graph->checkForCycles())
 		ptr += sprintf(ptr, "[mo cycle]");
-	if (priv->failed_promise)
+	if (priv->failed_promise || priv->hard_failed_promise)
 		ptr += sprintf(ptr, "[failed promise]");
 	if (priv->too_many_reads)
 		ptr += sprintf(ptr, "[too many reads]");
@@ -1397,7 +1399,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const
  */
 bool ModelExecution::is_feasible_prefix_ignore_relseq() const
 {
-	return !is_infeasible() && promises.size() == 0;
+	return !is_infeasible() && promises.size() == 0 && ! priv->failed_promise;
+
 }
 
 /**
@@ -1410,9 +1413,9 @@ bool ModelExecution::is_infeasible() const
 {
 	return mo_graph->checkForCycles() ||
 		priv->no_valid_reads ||
-		priv->failed_promise ||
 		priv->too_many_reads ||
 		priv->bad_synchronization ||
+		priv->hard_failed_promise ||
 		promises_expired();
 }
 
@@ -1769,7 +1772,8 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAc
 				   pendingfuturevalue.
 
 				 */
-				if (send_fv && thin_air_constraint_may_allow(curr, act)) {
+
+				if (send_fv && thin_air_constraint_may_allow(curr, act) && check_coherence_promise(curr, act)) {
 					if (!is_infeasible())
 						send_fv->push_back(act);
 					else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
@@ -1791,6 +1795,50 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAc
 	return added;
 }
 
+//This procedure uses cohere to prune future values that are
+//guaranteed to generate a coherence violation.
+//
+//need to see if there is (1) a promise for thread write, (2)
+//the promise is sb before write, (3) the promise can only be
+//resolved by the thread read, and (4) the promise has same
+//location as read/write
+
+bool ModelExecution::check_coherence_promise(const ModelAction * write, const ModelAction *read) {
+	thread_id_t write_tid=write->get_tid();
+	for(unsigned int i = promises.size(); i>0; i--) {
+		Promise *pr=promises[i-1];
+		if (!pr->same_location(write))
+			continue;
+		//the reading thread is the only thread that can resolve the promise
+		if (pr->get_num_was_available_threads()==1 && pr->thread_was_available(read->get_tid())) {
+			for(unsigned int j=0;j<pr->get_num_readers();j++) {
+				ModelAction *prreader=pr->get_reader(j);
+				//the writing thread reads from the promise before the write
+				if (prreader->get_tid()==write_tid &&
+						(*prreader)<(*write)) {
+					if ((*read)>(*prreader)) {
+						//check that we don't have a read between the read and promise
+						//from the same thread as read
+						bool okay=false;
+						for(const ModelAction *tmp=read;tmp!=prreader;) {
+							tmp=tmp->get_node()->get_parent()->get_action();
+							if (tmp->is_read() && tmp->same_thread(read)) {
+								okay=true;
+								break;
+							}
+						}
+						if (okay)
+							continue;
+					}
+					return false;
+				}
+			}
+		}
+	}
+	return true;
+}
+
+
 /** Arbitrary reads from the future are not allowed.  Section 29.3
  * part 9 places some constraints.  This method checks one result of constraint
  * constraint.  Others require compiler support. */
@@ -2353,7 +2401,7 @@ bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise,
 	/* Make sure the promise's value matches the write's value */
 	ASSERT(promise->is_compatible(write) && promise->same_value(write));
 	if (!mo_graph->resolvePromise(promise, write))
-		priv->failed_promise = true;
+		priv->hard_failed_promise = true;
 
 	/**
 	 * @todo  It is possible to end up in an inconsistent state, where a
@@ -2465,7 +2513,7 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec
 			if (!pread->happens_before(act))
 			       continue;
 			if (mo_graph->checkPromise(write, promise)) {
-				priv->failed_promise = true;
+				priv->hard_failed_promise = true;
 				return;
 			}
 			break;
@@ -2477,7 +2525,7 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec
 
 		if (mo_graph->checkReachable(promise, write)) {
 			if (mo_graph->checkPromise(write, promise)) {
-				priv->failed_promise = true;
+				priv->hard_failed_promise = true;
 				return;
 			}
 		}