From: bdemsky <bdemsky@uci.edu>
Date: Sat, 25 Jan 2014 22:11:22 +0000 (-0800)
Subject: Bug fix for broken treatment of promises + coherence based pruning to regain pruning... 
X-Git-Tag: oopsla2015~7
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6014243b7130f34b7ffd1098da225b0b8de5c328;p=model-checker.git

Bug fix for broken treatment of promises + coherence based pruning to regain pruning lost by bug fix
---

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 7e5e956..def51f9 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -456,9 +456,8 @@ bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) cons
 
 		if (node->getPromise() == promise)
 			return true;
-		if (!node->is_promise() &&
-				promise->eliminate_thread(node->getAction()->get_tid()))
-			return true;
+		if (!node->is_promise())
+			promise->eliminate_thread(node->getAction()->get_tid());
 
 		for (unsigned int i = 0; i < node->getNumEdges(); i++) {
 			CycleNode *next = node->getEdge(i);
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;
 			}
 		}
diff --git a/execution.h b/execution.h
index 9c9c1ca..2ca2513 100644
--- a/execution.h
+++ b/execution.h
@@ -187,7 +187,7 @@ private:
 	void propagate_clockvector(ModelAction *acquire, work_queue_t *work);
 	bool resolve_release_sequences(void *location, work_queue_t *work_queue);
 	void add_future_value(const ModelAction *writer, ModelAction *reader);
-
+	bool check_coherence_promise(const ModelAction *write, const ModelAction *read);
 	ModelAction * get_uninitialized_action(const ModelAction *curr) const;
 
 	action_list_t action_trace;
diff --git a/promise.cc b/promise.cc
index 3a38384..a98403b 100644
--- a/promise.cc
+++ b/promise.cc
@@ -16,6 +16,7 @@
 Promise::Promise(const ModelExecution *execution, ModelAction *read, struct future_value fv) :
 	execution(execution),
 	num_available_threads(0),
+	num_was_available_threads(0),
 	fv(fv),
 	readers(1, read),
 	write(NULL)
@@ -82,6 +83,12 @@ void Promise::add_thread(thread_id_t tid)
 		available_thread[id] = true;
 		num_available_threads++;
 	}
+	if (id >= was_available_thread.size())
+		was_available_thread.resize(id + 1, false);
+	if (!was_available_thread[id]) {
+		was_available_thread[id] = true;
+		num_was_available_threads++;
+	}
 }
 
 /**
@@ -100,6 +107,14 @@ bool Promise::thread_is_available(thread_id_t tid) const
 	return available_thread[id];
 }
 
+bool Promise::thread_was_available(thread_id_t tid) const
+{
+	unsigned int id = id_to_int(tid);
+	if (id >= was_available_thread.size())
+		return false;
+	return was_available_thread[id];
+}
+
 /**
  * @brief Get an upper bound on the number of available threads
  *
diff --git a/promise.h b/promise.h
index 84d5aa4..e306e14 100644
--- a/promise.h
+++ b/promise.h
@@ -31,11 +31,13 @@ class Promise {
 	bool eliminate_thread(thread_id_t tid);
 	void add_thread(thread_id_t tid);
 	bool thread_is_available(thread_id_t tid) const;
+	bool thread_was_available(thread_id_t tid) const;
 	unsigned int max_available_thread_idx() const;
 	bool has_failed() const;
 	void set_write(const ModelAction *act) { write = act; }
 	const ModelAction * get_write() const { return write; }
 	int get_num_available_threads() const { return num_available_threads; }
+	int get_num_was_available_threads() const { return num_was_available_threads; }
 	bool is_compatible(const ModelAction *act) const;
 	bool is_compatible_exclusive(const ModelAction *act) const;
 	bool same_value(const ModelAction *write) const;
@@ -60,8 +62,10 @@ class Promise {
 	/** @brief Thread ID(s) for thread(s) that potentially can satisfy this
 	 *  promise */
 	SnapVector<bool> available_thread;
+	SnapVector<bool> was_available_thread;
 
 	int num_available_threads;
+	int num_was_available_threads;
 
 	const future_value fv;