From: Brian Norris <banorris@uci.edu>
Date: Thu, 1 Nov 2012 17:38:49 +0000 (-0700)
Subject: model: update mo_may_allow restrictions
X-Git-Tag: pldi2013~34
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=d5c56ae55e7adf3e489de357ed5c80c640b67ec9

model: update mo_may_allow restrictions

For future values, we can enforce the following rule:

  If X --hb-> Y --mo-> Z, then X should not read from Z.

This a change from previous behavior, where we used 'sb' instead of
'hb'.

Tested with linuxrwlocks example:

  ./run.sh test/linuxrwlocks.o -f 4 -m 1

No difference in number of executions (feasible or infeasible); HASH
values were exactly the same.
---

diff --git a/model.cc b/model.cc
index f8aa4f0..0ef825d 100644
--- a/model.cc
+++ b/model.cc
@@ -1366,32 +1366,40 @@ 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) {
+/**
+ * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
+ * some constraints. This method checks one the following constraint (others
+ * require compiler support):
+ *
+ *   If X --hb-> Y --mo-> Z, then X should not read from Z.
+ */
+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());
+	unsigned int i;
 
-	//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;
-	}
+	/* Iterate over all threads */
+	for (i = 0; i < thrd_lists->size(); i++) {
+		ModelAction *write_after_read = NULL;
 
-	if (first_write_after_read==NULL)
-		return true;
+		/* Iterate over actions in thread, starting from most recent */
+		action_list_t *list = &(*thrd_lists)[i];
+		action_list_t::reverse_iterator rit;
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *act = *rit;
 
-	return !mo_graph->checkReachable(first_write_after_read, writer);
-}
+			if (!reader->happens_before(act))
+				break;
+			else if (act->is_write())
+				write_after_read = act;
+		}
 
+		if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+			return false;
+	}
 
+	return true;
+}
 
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.