projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
04d2bd9
)
fix mistake in promises may allow code... need to be even more aggressive about fv
author
Brian Demsky
<bdemsky@uci.edu>
Fri, 22 Mar 2013 07:06:51 +0000
(
00:06
-0700)
committer
Brian Norris
<banorris@uci.edu>
Fri, 22 Mar 2013 17:06:52 +0000
(10:06 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 167ea947a79a020964ec13fc67d67077aae961f7..7df70eebbe271c88486a4c85e4289217f1a40e4b 100644
(file)
--- 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
*
* 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
* 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
{
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;
}
/**
}
/**