correct comment typo

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 32be0538a9077d17951911cb01be66accacbb266..7df70eebbe271c88486a4c85e4289217f1a40e4b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1051,6 +1051,37 @@ bool ModelChecker::process_mutex(ModelAction *curr)
        return false;
 }
 
+/**
+ * @brief Check if the current pending promises allow a future value to be sent
+ *
+ * If one of the following is true:
+ *  (a) there are no pending promises
+ *  (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
+ *
+ * @param writer The operation which sends the future value. Must be a write.
+ * @param reader The operation which will observe the value. Must be a read.
+ * @return True if the future value can be sent now; false if it must wait.
+ */
+bool ModelChecker::promises_may_allow(const ModelAction *writer,
+               const ModelAction *reader) const
+{
+       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;
+}
+
 /**
  * @brief Add a future value to a reader
  *
@@ -1104,19 +1135,27 @@ bool ModelChecker::process_write(ModelAction *curr)
        } else
                earliest_promise_reader = NULL;
 
-       /* Don't send future values to reads after the Promise we resolve */
        for (unsigned int i = 0; i < send_fv.size(); i++) {
                ModelAction *read = send_fv[i];
-               if (!earliest_promise_reader || *read < *earliest_promise_reader)
-                       futurevalues->push_back(PendingFutureValue(curr, read));
+
+               /* Don't send future values to reads after the Promise we resolve */
+               if (!earliest_promise_reader || *read < *earliest_promise_reader) {
+                       /* Check if future value can be sent immediately */
+                       if (promises_may_allow(curr, read)) {
+                               add_future_value(curr, read);
+                       } else {
+                               futurevalues->push_back(PendingFutureValue(curr, read));
+                       }
+               }
        }
 
-       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();