From 307520433027a3e7440d1b3e34c52e1adbf2b05a Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 11 Sep 2012 10:20:06 -0700
Subject: [PATCH] model: add check_recency()

Note the weaknesses of the code, as documented in @todo.
---
 model.cc | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 model.h  |  1 +
 2 files changed, 53 insertions(+)

diff --git a/model.cc b/model.cc
index c77d4e1..cbabe71 100644
--- a/model.cc
+++ b/model.cc
@@ -329,6 +329,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			value = reads_from->get_value();
 			/* Assign reads_from, perform release/acquire synchronization */
 			curr->read_from(reads_from);
+			check_recency(curr, already_added);
+
 			if (r_modification_order(curr,reads_from))
 				updated = true;
 		} else {
@@ -400,6 +402,56 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 	return lastread;
 }
 
+/**
+ * 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.
+ */
+void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
+	if (params.maxreads != 0) {
+		if (curr->get_node()->get_read_from_size() <= 1)
+			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());
+
+		/* Skip checks */
+		if ((int)thrd_lists->size() <= tid)
+			return;
+
+		action_list_t *list = &(*thrd_lists)[tid];
+
+		action_list_t::reverse_iterator rit = list->rbegin();
+		/* Skip past curr */
+		if (!already_added) {
+			for (; (*rit) != curr; rit++)
+				;
+			/* go past curr now */
+			rit++;
+		}
+
+		int count=0;
+		for (; rit != list->rend(); rit++) {
+			ModelAction *act = *rit;
+			if (!act->is_read())
+				return;
+			if (act->get_reads_from() != curr->get_reads_from())
+				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 */
+				too_many_reads = true;
+			}
+		}
+	}
+}
+
 /**
  * Updates the mo_graph with the constraints imposed from the current read.
  * @param curr The current action. Must be a read.
diff --git a/model.h b/model.h
index 5d34b4a..70ec804 100644
--- a/model.h
+++ b/model.h
@@ -104,6 +104,7 @@ private:
 
 	bool take_step();
 
+	void check_recency(ModelAction *curr, bool already_added);
 	ModelAction * get_last_conflict(ModelAction *act);
 	void set_backtracking(ModelAction *act);
 	Thread * get_next_replay_thread();
-- 
2.34.1