From: Brian Demsky <bdemsky@uci.edu>
Date: Mon, 10 Sep 2012 00:43:20 +0000 (-0700)
Subject: model: fix the maxreads support
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=fa47e498d6eb6a97d25bc255df1c08bf66bc4c40

model: fix the maxreads support
---

diff --git a/model.cc b/model.cc
index b5a29dd5..2be1c82e 100644
--- a/model.cc
+++ b/model.cc
@@ -416,19 +416,26 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 }
 
 /**
- * Checks whether a thread has read from the same write for too many times.
- * @todo This may be more subtle than this code segment addresses at this
- * point...  Potential problems to ponder and fix:
- * (1) What if the reads_from set keeps changing such that there is no common
- * write?
- * (2) What if the problem is that the other writes would break modification
- * order.
+ * Checks whether a thread has read from the same write for too many times
+ * without seeing the effects of a later write.
+ *
+ * Basic idea:
+ * 1) there must a different write that we could read from that would satisfy the modification order,
+ * 2) we must have read from the same value in excess of maxreads times, and
+ * 3) that other write must have been in the reads_from set for maxreads times.
+ *
+ * If so, we decide that the execution is no longer feasible.
  */
 void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
 	if (params.maxreads != 0) {
 		if (curr->get_node()->get_read_from_size() <= 1)
 			return;
 
+		//Must make sure that execution is currently feasible...  We could
+		//accidentally clear by rolling back
+		if (!isfeasible())
+			return;
+
 		std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 		int tid = id_to_int(curr->get_tid());
 
@@ -447,8 +454,12 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
 			rit++;
 		}
 
+		action_list_t::reverse_iterator ritcopy=rit;
+		//See if we have enough reads from the same value
 		int count=0;
-		for (; rit != list->rend(); rit++) {
+		for (; count < params.maxreads; rit++,count++) {
+			if (rit==list->rend())
+				return;
 			ModelAction *act = *rit;
 			if (!act->is_read())
 				return;
@@ -456,10 +467,44 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
 				return;
 			if (act->get_node()->get_read_from_size() <= 1)
 				return;
-			count++;
-			if (count >= params.maxreads) {
-				/* We've read from the same write for too many times */
+		}
+
+		for (int i=0;i<curr->get_node()->get_read_from_size();i++) {
+			//Get write
+			const ModelAction * write=curr->get_node()->get_read_from_at(i);
+			//Need a different write
+			if (write==curr->get_reads_from())
+				continue;
+
+			/* Test to see whether this is a feasible write to read from*/
+			r_modification_order(curr, write);
+			bool feasiblereadfrom=isfeasible();
+			mo_graph->rollbackChanges();
+
+			if (!feasiblereadfrom)
+				continue;
+			rit=ritcopy;
+
+			bool feasiblewrite=true;
+			//new we need to see if this write works for everyone
+
+			for (int loop=count;loop>0;loop--,rit++) {
+				ModelAction *act=*rit;
+				bool foundvalue=false;
+				for(int j=0;j<act->get_node()->get_read_from_size();j++) {
+					if (act->get_node()->get_read_from_at(i)==write) {
+						foundvalue=true;
+						break;
+					}
+				}
+				if (!foundvalue) {
+					feasiblewrite=false;
+					break;
+				}
+			}
+			if (feasiblewrite) {
 				too_many_reads = true;
+				return;
 			}
 		}
 	}
diff --git a/nodestack.cc b/nodestack.cc
index 71af6ef2..a9399edb 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -225,6 +225,10 @@ int Node::get_read_from_size() {
 	return may_read_from.size();
 }
 
+const ModelAction * Node::get_read_from_at(int i) {
+	return may_read_from[i];
+}
+
 /**
  * Gets the next 'may_read_from' action from this Node. Only valid for a node
  * where this->action is a 'read'.
diff --git a/nodestack.h b/nodestack.h
index 8b4d7aef..b391645b 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -65,6 +65,7 @@ public:
 	bool increment_read_from();
 	bool read_from_empty();
 	int get_read_from_size();
+	const ModelAction * get_read_from_at(int i);
 
 	void set_promise(unsigned int i);
 	bool get_promise(unsigned int i);