X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=691ab832519d11dff2515dfe313884da05ef7382;hb=fbacb5f41ada96e7b539ccc41deccb1a7e1a1ba8;hp=6739d2c85ee2ca51dd3963c471c811e12f0711b3;hpb=ae1340cbd7d2f75d76a4199597f454290badcc8b;p=model-checker.git

diff --git a/model.cc b/model.cc
index 6739d2c..691ab83 100644
--- a/model.cc
+++ b/model.cc
@@ -1808,6 +1808,15 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 		}
 	}
 
+	/*
+	 * All compatible, thread-exclusive promises must be ordered after any
+	 * concrete stores to the same thread, or else they can be merged with
+	 * this store later
+	 */
+	for (unsigned int i = 0; i < promises->size(); i++)
+		if ((*promises)[i]->is_compatible_exclusive(curr))
+			added = mo_graph->addEdge(curr, (*promises)[i]) || added;
+
 	return added;
 }