projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
6014243
)
bug fix with missing coherence condition for promises
author
bdemsky
<bdemsky@uci.edu>
Wed, 16 Apr 2014 22:01:00 +0000
(15:01 -0700)
committer
bdemsky
<bdemsky@uci.edu>
Wed, 16 Apr 2014 22:01:00 +0000
(15:01 -0700)
execution.cc
patch
|
blob
|
history
diff --git
a/execution.cc
b/execution.cc
index 3a630d777f060cb22598858278044d6e140cfed3..01a5fa442b0905b522f05714d95dc7eaf5fa56a2 100644
(file)
--- 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
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) &&
}
break;
} else if (act->is_read() && !act->could_synchronize_with(curr) &&