model: bugfix - send future values more eagerly

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 7ce959e90b9c5aeaf649df1f422868a63aa34421..a9d90914afbbe5205cabc01513b25082d4ca2e4b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1051,25 +1051,56 @@ 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
+ *
+ * This function performs a few additional checks to ensure that the future
+ * value can be feasibly observed by the reader
+ *
+ * @param writer The operation whose value is sent. Must be a write.
+ * @param reader The read operation which may read the future value. Must be a read.
+ */
 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
 {
        /* Do more ambitious checks now that mo is more complete */
-       if (mo_may_allow(writer, reader)) {
-               Node *node = reader->get_node();
-
-               /* Find an ancestor thread which exists at the time of the reader */
-               Thread *write_thread = get_thread(writer);
-               while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
-                       write_thread = write_thread->get_parent();
-
-               struct future_value fv = {
-                       writer->get_write_value(),
-                       writer->get_seq_number() + params.maxfuturedelay,
-                       write_thread->get_id(),
-               };
-               if (node->add_future_value(fv))
-                       set_latest_backtrack(reader);
-       }
+       if (!mo_may_allow(writer, reader))
+               return;
+
+       Node *node = reader->get_node();
+
+       /* Find an ancestor thread which exists at the time of the reader */
+       Thread *write_thread = get_thread(writer);
+       while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
+               write_thread = write_thread->get_parent();
+
+       struct future_value fv = {
+               writer->get_write_value(),
+               writer->get_seq_number() + params.maxfuturedelay,
+               write_thread->get_id(),
+       };
+       if (node->add_future_value(fv))
+               set_latest_backtrack(reader);
 }
 
 /**
@@ -1094,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()) {