From ee0f520bb244e2aa820e6b5a7e24c43c396b0905 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Mon, 8 Oct 2012 23:35:21 -0700
Subject: [PATCH] did a little more looking at infeasible executions... another
 obvious property we missed...kills about 1/3 of the infeasible executions...

---
 model.cc | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/model.cc b/model.cc
index e11dcf7..ee3ce99 100644
--- a/model.cc
+++ b/model.cc
@@ -1779,6 +1779,11 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
 			//do we have a pwrite for the promise, if not, set it
 			if (promise->get_write() == NULL ) {
 				promise->set_write(write);
+				//The pwrite cannot happen before the promise
+				if (write->happens_before(act) && (write != act)) {
+					failed_promise = true;
+					return;
+				}
 			}
 			if (mo_graph->checkPromise(write, promise)) {
 				failed_promise = true;
-- 
2.34.1