From 262fab229626c8504297467fc7b5a04f60b7c530 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Fri, 22 Mar 2013 00:06:51 -0700 Subject: [PATCH] fix mistake in promises may allow code... need to be even more aggressive about fv --- model.cc | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/model.cc b/model.cc index 167ea947..7df70eeb 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; } /** -- 2.34.1