From d27984bb297795f4e9a4531e2730d8188a799e89 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Mon, 8 Oct 2012 17:19:32 -0700
Subject: [PATCH] be much more careful about sending values backwards...

also implement hashing for traces...just an easy way to confirm whether we lose new traces...
---
 action.cc | 15 +++++++++++++++
 action.h  |  1 +
 model.cc  | 48 +++++++++++++++++++++++++++++++++++++++++++-----
 model.h   |  4 ++--
 4 files changed, 61 insertions(+), 7 deletions(-)

diff --git a/action.cc b/action.cc
index b7bf024..3aeb737 100644
--- a/action.cc
+++ b/action.cc
@@ -415,3 +415,18 @@ void ModelAction::print() const
 	} else
 		printf("\n");
 }
+
+/** @brief Print nicely-formatted info about this ModelAction */
+unsigned int ModelAction::hash() const
+{
+	unsigned int hash=(unsigned int) this->type;
+	hash^=((unsigned int)this->order)<<3;
+	hash^=seq_number<<5;
+	hash^=tid<<6;
+
+	if (is_read()) {
+		if (reads_from)
+			hash^=reads_from->get_seq_number();
+	}
+	return hash;
+}
diff --git a/action.h b/action.h
index 68db2c3..4960931 100644
--- a/action.h
+++ b/action.h
@@ -127,6 +127,7 @@ public:
 
 	void set_sleep_flag() { sleep_flag=true; }
 	bool get_sleep_flag() { return sleep_flag; }
+	unsigned int hash() const;
 
 	MEMALLOC
 private:
diff --git a/model.cc b/model.cc
index f8482cb..7e8211d 100644
--- a/model.cc
+++ b/model.cc
@@ -519,7 +519,9 @@ bool ModelChecker::process_write(ModelAction *curr)
 	if (promises->size() == 0) {
 		for (unsigned int i = 0; i < futurevalues->size(); i++) {
 			struct PendingFutureValue pfv = (*futurevalues)[i];
-			if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
+			//Do more ambitious checks now that mo is more complete
+			if (mo_may_allow(pfv.writer, pfv.act)&&
+					pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
 					(!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
 				priv->next_backtrack = pfv.act;
 		}
@@ -1248,12 +1250,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				   (3) cannot synchronize with us
 				   (4) is in a different thread
 				   =>
-				   that read could potentially read from our write.
+				   that read could potentially read from our write.  Note that
+				   these checks are overly conservative at this point, we'll
+				   do more checks before actually removing the
+				   pendingfuturevalue.
+
 				 */
 				if (thin_air_constraint_may_allow(curr, act)) {
 					if (isfeasible() ||
 							(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
-						struct PendingFutureValue pfv = {curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act};
+						struct PendingFutureValue pfv = {curr,act};
 						futurevalues->push_back(pfv);
 					}
 				}
@@ -1285,6 +1291,34 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
 	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. */
+bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
+	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+
+	//Get write that follows reader action
+	action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
+	action_list_t::reverse_iterator rit;
+	ModelAction *first_write_after_read=NULL;
+
+	for (rit = list->rbegin(); rit != list->rend(); rit++) {
+		ModelAction *act = *rit;
+		if (act==reader)
+			break;
+		if (act->is_write())
+			first_write_after_read=act;
+	}
+
+	if (first_write_after_read==NULL)
+		return true;
+	return true;
+
+	//return !mo_graph->checkReachable(first_write_after_read, writer);
+}
+
+
+
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
  * The ModelAction under consideration is expected to be taking part in
@@ -1885,8 +1919,9 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr
 		bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
 		if (write->is_release()&&thread_sleep)
 			return true;
-		if (!write->is_rmw())
+		if (!write->is_rmw()) {
 			return false;
+		}
 		if (write->get_reads_from()==NULL)
 			return true;
 		write=write->get_reads_from();
@@ -1899,10 +1934,13 @@ static void print_list(action_list_t *list)
 
 	printf("---------------------------------------------------------------------\n");
 	printf("Trace:\n");
-
+	unsigned int hash=0;
+	
 	for (it = list->begin(); it != list->end(); it++) {
 		(*it)->print();
+		hash=hash^(hash<<3)^((*it)->hash());
 	}
+	printf("HASH %u\n", hash);
 	printf("---------------------------------------------------------------------\n");
 }
 
diff --git a/model.h b/model.h
index 8316f04..c99e0f8 100644
--- a/model.h
+++ b/model.h
@@ -39,8 +39,7 @@ struct model_params {
 };
 
 struct PendingFutureValue {
-	uint64_t value;
-	modelclock_t expiration;
+	ModelAction *writer;
 	ModelAction * act;
 };
 
@@ -120,6 +119,7 @@ private:
 
 	bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
 	bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
+	bool mo_may_allow(const ModelAction * writer, const ModelAction *reader);
 	bool has_asserted() {return asserted;}
 	void reset_asserted() {asserted=false;}
 	int num_executions;
-- 
2.34.1