promise: record multiple readers in the same Promise

This requires more adjustments throughout ModelChecker.

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 1dbb12d9d25e2179895554817133b1c0267f179d..67552e0068f5f6d96e11169b4c0a60557d7c879d 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -320,7 +320,7 @@ static void print_node(const CycleNode *node, FILE *file, int label)
        modelclock_t idx;
        if (node->is_promise()) {
                const Promise *promise = node->getPromise();
-               idx = promise->get_action()->get_seq_number();
+               idx = promise->get_reader(0)->get_seq_number();
                fprintf(file, "P%u", idx);
                if (label) {
                        int first = 1;

diff --git a/model.cc b/model.cc
index 44fba7eabc84839bc71bc64e7b69f18bb123b676..38d63a2fcb9f0a45f850fc1b7bf718d1579bd234 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -873,6 +873,7 @@ bool ModelChecker::process_read(ModelAction *curr)
                }
                case READ_FROM_PROMISE: {
                        Promise *promise = curr->get_node()->get_read_from_promise();
+                       promise->add_reader(curr);
                        value = promise->get_value();
                        curr->set_read_from_promise(promise);
                        mo_graph->startChanges();
@@ -1348,14 +1349,19 @@ void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiti
 {
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
-               ModelAction *reader = promise->get_action();
-               if (reader->get_tid() != blocker->get_id())
-                       continue;
                if (!promise->thread_is_available(waiting->get_id()))
                        continue;
-               if (promise->eliminate_thread(waiting->get_id())) {
-                       /* Promise has failed */
-                       priv->failed_promise = true;
+               for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+                       ModelAction *reader = promise->get_reader(j);
+                       if (reader->get_tid() != blocker->get_id())
+                               continue;
+                       if (promise->eliminate_thread(waiting->get_id())) {
+                               /* Promise has failed */
+                               priv->failed_promise = true;
+                       } else {
+                               /* Only eliminate the 'waiting' thread once */
+                               return;
+                       }
                }
        }
 }
@@ -2451,15 +2457,17 @@ bool ModelChecker::resolve_promises(ModelAction *write)
        for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
                Promise *promise = (*promises)[promise_index];
                if (write->get_node()->get_promise(i)) {
-                       ModelAction *read = promise->get_action();
-                       read_from(read, write);
+                       for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+                               ModelAction *read = promise->get_reader(j);
+                               read_from(read, write);
+                               actions_to_check.push_back(read);
+                       }
                        //Make sure the promise's value matches the write's value
                        ASSERT(promise->is_compatible(write));
                        mo_graph->resolvePromise(promise, write, &mustResolve);
 
                        resolved.push_back(promise);
                        promises->erase(promises->begin() + promise_index);
-                       actions_to_check.push_back(read);
 
                        haveResolved = true;
                } else
@@ -2494,14 +2502,20 @@ void ModelChecker::compute_promises(ModelAction *curr)
 {
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
-               const ModelAction *act = promise->get_action();
-               ASSERT(act->is_read());
-               if (!act->happens_before(curr) &&
-                               !act->could_synchronize_with(curr) &&
-                               promise->is_compatible(curr) &&
-                               promise->get_value() == curr->get_value()) {
-                       curr->get_node()->set_promise(i);
+               if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value())
+                       continue;
+
+               bool satisfy = true;
+               for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+                       const ModelAction *act = promise->get_reader(j);
+                       if (act->happens_before(curr) ||
+                                       act->could_synchronize_with(curr)) {
+                               satisfy = false;
+                               break;
+                       }
                }
+               if (satisfy)
+                       curr->get_node()->set_promise(i);
        }
 }
 
@@ -2510,13 +2524,17 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
 {
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
-               const ModelAction *act = promise->get_action();
-               if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
-                               merge_cv->synchronized_since(act)) {
-                       if (promise->eliminate_thread(tid)) {
-                               //Promise has failed
-                               priv->failed_promise = true;
-                               return;
+               if (!promise->thread_is_available(tid))
+                       continue;
+               for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+                       const ModelAction *act = promise->get_reader(j);
+                       if ((!old_cv || !old_cv->synchronized_since(act)) &&
+                                       merge_cv->synchronized_since(act)) {
+                               if (promise->eliminate_thread(tid)) {
+                                       /* Promise has failed */
+                                       priv->failed_promise = true;
+                                       return;
+                               }
                        }
                }
        }
@@ -2553,15 +2571,20 @@ void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
 
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
-               const ModelAction *pread = promise->get_action();
 
                // Is this promise on the same location?
-               if (!pread->same_var(write))
+               if (promise->get_value() != write->get_value())
                        continue;
 
-               if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
-                       priv->failed_promise = true;
-                       return;
+               for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+                       const ModelAction *pread = promise->get_reader(j);
+                       if (!pread->happens_before(act))
+                              continue;
+                       if (mo_graph->checkPromise(write, promise)) {
+                               priv->failed_promise = true;
+                               return;
+                       }
+                       break;
                }
 
                // Don't do any lookups twice for the same thread
@@ -2656,7 +2679,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
        /* Inherit existing, promised future values */
        for (i = 0; i < promises->size(); i++) {
                const Promise *promise = (*promises)[i];
-               const ModelAction *promise_read = promise->get_action();
+               const ModelAction *promise_read = promise->get_reader(0);
                if (promise_read->same_var(curr)) {
                        /* Only add feasible future-values */
                        mo_graph->startChanges();

diff --git a/promise.cc b/promise.cc
index 86c3c584f12ba884d190c792b10f459e225c8330..23b92cd4186a59bb7a5b7c411668501afc4447e7 100644 (file)
--- a/promise.cc
+++ b/promise.cc
@@ -15,13 +15,38 @@
 Promise::Promise(ModelAction *read, struct future_value fv) :
        num_available_threads(0),
        fv(fv),
-       read(read),
+       readers(1, read),
        write(NULL)
 {
        add_thread(fv.tid);
        eliminate_thread(read->get_tid());
 }
 
+/**
+ * Add a reader that reads from this Promise. Must be added in an order
+ * consistent with execution order.
+ *
+ * @param reader The ModelAction that reads from this promise. Must be a read.
+ * @return True if this new reader has invalidated the promise; false otherwise
+ */
+bool Promise::add_reader(ModelAction *reader)
+{
+       readers.push_back(reader);
+       return eliminate_thread(reader->get_tid());
+}
+
+/**
+ * Access a reader that read from this Promise. Readers must be inserted in
+ * order by execution order, so they can be returned in this order.
+ *
+ * @param i The index of the reader to return
+ * @return The i'th reader of this Promise
+ */
+ModelAction * Promise::get_reader(unsigned int i) const
+{
+       return i < readers.size() ? readers[i] : NULL;
+}
+
 /**
  * Eliminate a thread which no longer can satisfy this promise. Once all
  * enabled threads have been eliminated, this promise is unresolvable.
@@ -76,7 +101,7 @@ bool Promise::thread_is_available(thread_id_t tid) const
 /** @brief Print debug info about the Promise */
 void Promise::print() const
 {
-       model_print("Promised value %#" PRIx64 ", read from thread %d, available threads to resolve: ", fv.value, id_to_int(read->get_tid()));
+       model_print("Promised value %#" PRIx64 ", first read from thread %d, available threads to resolve: ", fv.value, id_to_int(get_reader(0)->get_tid()));
        for (unsigned int i = 0; i < available_thread.size(); i++)
                if (available_thread[i])
                        model_print("[%d]", i);
@@ -102,7 +127,7 @@ bool Promise::has_failed() const
  */
 bool Promise::is_compatible(const ModelAction *act) const
 {
-       return thread_is_available(act->get_tid()) && read->same_var(act);
+       return thread_is_available(act->get_tid()) && get_reader(0)->same_var(act);
 }
 
 /**

diff --git a/promise.h b/promise.h
index c131d743aa185d2972cd2d1922fb7ac43d6c3c8d..5ea7dc58d0470a29a537985c6322f8792be1f856 100644 (file)
--- a/promise.h
+++ b/promise.h
@@ -24,7 +24,9 @@ struct future_value {
 class Promise {
  public:
        Promise(ModelAction *read, struct future_value fv);
-       ModelAction * get_action() const { return read; }
+       bool add_reader(ModelAction *reader);
+       ModelAction * get_reader(unsigned int i) const;
+       unsigned int get_num_readers() const { return readers.size(); }
        bool eliminate_thread(thread_id_t tid);
        void add_thread(thread_id_t tid);
        bool thread_is_available(thread_id_t tid) const;
@@ -54,8 +56,8 @@ class Promise {
 
        const future_value fv;
 
-       /** @brief The action which reads a promised value */
-       ModelAction * const read;
+       /** @brief The action(s) which read the promised future value */
+       std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > readers;
 
        const ModelAction *write;
 };