From: Brian Norris <banorris@uci.edu>
Date: Tue, 12 Mar 2013 17:47:41 +0000 (-0700)
Subject: model: bugfix - missing SC mo_graph edge
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=34aa82864b18e6f11d806ef77e4b992c2e19f370

model: bugfix - missing SC mo_graph edge

We must enforce a rule such as the following, derived from C++ Section
29.3, statement 3 (second subpoint):

if is_store(X) && is_seq_cst(X) && is_store(Y) && is_load(Z) &&
   is_seq_cst(Z) &&
   X --sc-> Z && Y --rf-> Z && X != Y
then
   X --mo-> Y

This has been checked (via manual test-case) to fix a bug which allowed
an inconsistent mo/sc/rf relationship.
---

diff --git a/model.cc b/model.cc
index a03ea462..d9ff365e 100644
--- a/model.cc
+++ b/model.cc
@@ -1812,6 +1812,9 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 
 	/* Last SC fence in the current thread */
 	ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+	ModelAction *last_sc_write = NULL;
+	if (curr->is_seqcst())
+		last_sc_write = get_last_seq_cst_write(curr);
 
 	/* Iterate over all threads */
 	for (i = 0; i < thrd_lists->size(); i++) {
@@ -1863,6 +1866,12 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 				}
 			}
 
+			/* C++, Section 29.3 statement 3 (second subpoint) */
+			if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
+				added = mo_graph->addEdge(act, rf) || added;
+				break;
+			}
+
 			/*
 			 * Include at most one act per-thread that "happens
 			 * before" curr
@@ -2463,8 +2472,11 @@ ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
 	action_list_t *list = get_safe_ptr_action(obj_map, location);
 	/* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
 	action_list_t::reverse_iterator rit;
-	for (rit = list->rbegin(); rit != list->rend(); rit++)
-		if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
+	for (rit = list->rbegin(); (*rit) != curr; rit++)
+		;
+	rit++; /* Skip past curr */
+	for ( ; rit != list->rend(); rit++)
+		if ((*rit)->is_write() && (*rit)->is_seqcst())
 			return *rit;
 	return NULL;
 }