*
* 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
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;
}
/**
}
}
- if (promises->empty()) {
- for (unsigned int i = 0; i < futurevalues->size(); i++) {
- struct PendingFutureValue pfv = (*futurevalues)[i];
+ /* Check the pending future values */
+ for (int i = (int)futurevalues->size() - 1; i >= 0; i--) {
+ struct PendingFutureValue pfv = (*futurevalues)[i];
+ if (promises_may_allow(pfv.writer, pfv.reader)) {
add_future_value(pfv.writer, pfv.reader);
+ futurevalues->erase(futurevalues->begin() + i);
}
- futurevalues->clear();
}
mo_graph->commitChanges();