From 963f325c5b5df37487e17c3a05f4d15efabb8870 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 26 Feb 2013 16:39:09 -0800 Subject: [PATCH] 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. --- model.cc | 14 +++++++------- promise.h | 3 +++ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/model.cc b/model.cc index 4461379..bfb63e4 100644 --- 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 { - 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; diff --git a/promise.h b/promise.h index 5b0e356..c131d74 100644 --- a/promise.h +++ b/promise.h @@ -41,6 +41,9 @@ class Promise { 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 -- 2.34.1