From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 22 Mar 2013 07:06:51 +0000 (-0700)
Subject: fix mistake in promises may allow code...  need to be even more aggressive about fv
X-Git-Tag: oopsla2013~123
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=262fab229626c8504297467fc7b5a04f60b7c530

fix mistake in promises may allow code...  need to be even more aggressive about fv
---

diff --git a/model.cc b/model.cc
index 167ea94..7df70ee 100644
--- a/model.cc
+++ b/model.cc
@@ -1056,7 +1056,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
  *
  * If one of the following is true:
  *  (a) there are no pending promises
- *  (b) the reader is ordered after the latest Promise creation
+ *  (b) the reader and writer do not cross any promises
  * Then, it is safe to pass a future value back now.
  *
  * Otherwise, we must save the pending future value until (a) or (b) is true
@@ -1068,8 +1068,18 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 bool ModelChecker::promises_may_allow(const ModelAction *writer,
 		const ModelAction *reader) const
 {
-	return promises->empty() ||
-		*(promises->back()->get_reader(0)) < *reader;
+	if (promises->empty())
+		return true;
+	for(int i=promises->size()-1;i>=0;i--) {
+		ModelAction *pr=(*promises)[i]->get_reader(0);
+		//reader is after promise...doesn't cross any promise
+		if (*reader > *pr)
+			return true;
+		//writer is after promise, reader before...bad...
+		if (*writer > *pr)
+			return false;
+	}
+	return true;
 }
 
 /**