model: bugfix - send future values more eagerly

This is a bugfix to a pretty big problem with our future value pruning,
where we would hold future values as 'pending' until all pending
promises were resolved. Unfortunately, this is unsound and must be
rewritten.

Now, we allow sending some future values even in presence of promises,
if the value is being sent to a load that is later than the last time a
Promise was created. We have a pseudo-proof that this should be correct.

diff --git a/model.cc b/model.cc
index 32be0538a9077d17951911cb01be66accacbb266..a9d90914afbbe5205cabc01513b25082d4ca2e4b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1051,6 +1051,27 @@ 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 is ordered after the latest Promise creation
+ * 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
+{
+       return promises->empty() ||
+               *(promises->back()->get_reader(0)) < *reader;
+}
+
 /**
  * @brief Add a future value to a reader
  *
@@ -1104,11 +1125,18 @@ 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()) {

diff --git a/model.h b/model.h
index 3e9d0643d5e4f7496cb5b51bd8fd8a42ac31c505..355764b7c4d290cfb3de64f7f0c0086a0ba83c73 100644 (file)
--- a/model.h
+++ b/model.h
@@ -148,6 +148,7 @@ private:
        bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
        bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
+       bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        bool has_asserted() const;
        void set_assert();
        void set_bad_synchronization();