model: bugfix - correct RR coherence for Promises

We should not skip a read just because it has an unresolved promises;
the CycleGraph can now support read-read coherence edges between any
combination of Promise and ModelAction.

diff --git a/model.cc b/model.cc
index 446137922bbce9b56aa37c092db174a0dc3df71f..bfb63e48ddd5d0d9ac0bc096b3604d3e6d9e640d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1765,13 +1765,13 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                                                added = mo_graph->addEdge(act, rf) || added;
                                        }
                                } else {
                                                added = mo_graph->addEdge(act, rf) || added;
                                        }
                                } else {

-                                       const ModelAction *prevreadfrom = act->get_reads_from();
-                                       //if the previous read is unresolved, keep going...
-                                       if (prevreadfrom == NULL)
-                                               continue;
-
-                                       if (!prevreadfrom->equals(rf)) {
-                                               added = mo_graph->addEdge(prevreadfrom, rf) || added;
+                                       const ModelAction *prevrf = act->get_reads_from();
+                                       const Promise *prevrf_promise = act->get_reads_from_promise();
+                                       if (prevrf) {
+                                               if (!prevrf->equals(rf))
+                                                       added = mo_graph->addEdge(prevrf, rf) || added;
+                                       } else if (!prevrf->equals(rf)) {
+                                               added = mo_graph->addEdge(prevrf_promise, rf) || added;

                                        }
                                }
                                break;
                                        }
                                }
                                break;

diff --git a/promise.h b/promise.h
index 5b0e356bc6873238765577cab957977dc8c8a143..c131d743aa185d2972cd2d1922fb7ac43d6c3c8d 100644 (file)
--- a/promise.h
+++ b/promise.h
@@ -41,6 +41,9 @@ class Promise {
 
        void print() const;
 
 
        void print() const;
 

+       bool equals(const Promise *x) const { return this == x; }
+       bool equals(const ModelAction *x) const { return false; }
+

        SNAPSHOTALLOC
  private:
        /** @brief Thread ID(s) for thread(s) that potentially can satisfy this
        SNAPSHOTALLOC
  private:
        /** @brief Thread ID(s) for thread(s) that potentially can satisfy this