From: bdemsky <bdemsky@uci.edu>
Date: Wed, 16 Apr 2014 22:01:00 +0000 (-0700)
Subject: bug fix with missing coherence condition for promises
X-Git-Tag: oopsla2015~6
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=3fe3c730dd6a8deb536276f7a68ef58cae0d74f3

bug fix with missing coherence condition for promises
---

diff --git a/execution.cc b/execution.cc
index 3a630d7..01a5fa4 100644
--- a/execution.cc
+++ b/execution.cc
@@ -1753,9 +1753,10 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAc
 					added = mo_graph->addEdge(act, curr) || added;
 				else if (act->is_read()) {
 					//if previous read accessed a null, just keep going
-					if (act->get_reads_from() == NULL)
-						continue;
-					added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
+					if (act->get_reads_from() == NULL) {
+						added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added;
+					} else
+						added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
 				}
 				break;
 			} else if (act->is_read() && !act->could_synchronize_with(curr) &&