model: re-check pending future values whenever a promise is resolved
authorBrian Norris <banorris@uci.edu>
Thu, 21 Mar 2013 23:48:57 +0000 (16:48 -0700)
committerBrian Norris <banorris@uci.edu>
Fri, 22 Mar 2013 01:03:34 +0000 (18:03 -0700)
This is the second part of the previous bugfix; now we must also allow
stashed pending future values to be re-checked in case a promise has
been resolved which now allows sending the value.

model.cc

index a9d9091..167ea94 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1139,12 +1139,13 @@ bool ModelChecker::process_write(ModelAction *curr)
                }
        }
 
-       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();