From: Brian Norris <banorris@uci.edu>
Date: Sat, 2 Mar 2013 20:17:02 +0000 (-0800)
Subject: check_recency: improve templates, use when reading from Promise
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=57f11820dd7dc4c3b95459a8de99305ac31f88bf;ds=sidebyside

check_recency: improve templates, use when reading from Promise

This completes (?) the improvements to check_recency, such that it now
can force new writes to be "seen" if we are reading from an "old"
Promise too many times in a row.

mpmc-queue-noinit now runs to completion (with ASSERT() enabled):

  $ time ./run.sh mpmc-queue/mpmc-queue-noinit -f 10 -m 2
  + mpmc-queue/mpmc-queue-noinit -f 10 -m 2
  ******* Model-checking complete: *******
  Number of complete, bug-free executions: 119828
  Number of redundant executions: 38743
  Number of buggy executions: 0
  Number of infeasible executions: 344469
  Total executions: 503040
  Total nodes created: 7585797

  real	2m29.674s
  user	2m18.269s
  sys	0m10.929s
---

diff --git a/model.cc b/model.cc
index b0ca05ea..5a1f3992 100644
--- a/model.cc
+++ b/model.cc
@@ -887,6 +887,8 @@ bool ModelChecker::process_read(ModelAction *curr)
 			value = promise->get_value();
 			curr->set_read_from_promise(promise);
 			mo_graph->startChanges();
+			if (!check_recency(curr, promise))
+				priv->too_many_reads = true;
 			updated = r_modification_order(curr, promise);
 			mo_graph->commitChanges();
 			break;
@@ -1642,8 +1644,8 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 	return lastread;
 }
 
-template <typename T>
-bool ModelChecker::should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const
+template <typename T, typename U>
+bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const
 {
 	/* Need a different write/promise */
 	if (other_rf->equals(rf))
@@ -1681,10 +1683,11 @@ bool ModelChecker::should_read_instead(const ModelAction *curr, const ModelActio
  * If so, we decide that the execution is no longer feasible.
  *
  * @param curr The current action. Must be a read.
- * @param rf The store from which we might read.
+ * @param rf The ModelAction/Promise from which we might read.
  * @return True if the read should succeed; false otherwise
  */
-bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const
+template <typename T>
+bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
 {
 	if (!params.maxreads)
 		return true;
diff --git a/model.h b/model.h
index 3f4ca001..d8c1be49 100644
--- a/model.h
+++ b/model.h
@@ -167,10 +167,11 @@ private:
 
 	Thread * take_step(ModelAction *curr);
 
-	bool check_recency(ModelAction *curr, const ModelAction *rf) const;
-
 	template <typename T>
-	bool should_read_instead(const ModelAction *curr, const ModelAction *rf, const T *other_rf) const;
+	bool check_recency(ModelAction *curr, const T *rf) const;
+
+	template <typename T, typename U>
+	bool should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const;
 
 	ModelAction * get_last_fence_conflict(ModelAction *act) const;
 	ModelAction * get_last_conflict(ModelAction *act) const;