projects
/
cdsspec-compiler.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
718fed5
)
another bug fix
author
Brian Demsky
<bdemsky@uci.edu>
Mon, 1 Oct 2012 23:27:49 +0000
(16:27 -0700)
committer
Brian Demsky
<bdemsky@uci.edu>
Mon, 1 Oct 2012 23:27:49 +0000
(16:27 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 62e75205e4ee9681bcef321856c744978c9cc5c1..468900aeb6120f659124e09fc839ac8aa53416ee 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-951,10
+951,10
@@
void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
action_list_t::reverse_iterator rit;
ModelAction *lastact = NULL;
action_list_t::reverse_iterator rit;
ModelAction *lastact = NULL;
- /* Find last action that happens after curr */
+ /* Find last action that happens after curr
that is either not curr or a rmw
*/
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (curr->happens_before(act)) {
+ if (curr->happens_before(act)
&& (curr != act || curr->is_rmw())
) {
lastact = act;
} else
break;
lastact = act;
} else
break;
@@
-962,12
+962,25
@@
void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
/* Include at most one act per-thread that "happens before" curr */
if (lastact != NULL) {
/* Include at most one act per-thread that "happens before" curr */
if (lastact != NULL) {
- if (lastact->is_read()) {
+ if (lastact==curr) {
+ //Case 1: The resolved read is a RMW, and we need to make sure
+ //that the write portion of the RMW mod order after rf
+
+ mo_graph->addEdge(rf, lastact);
+ } else if (lastact->is_read()) {
+ //Case 2: The resolved read is a normal read and the next
+ //operation is a read, and we need to make sure the value read
+ //is mod ordered after rf
+
const ModelAction *postreadfrom = lastact->get_reads_from();
if (postreadfrom != NULL&&rf != postreadfrom)
mo_graph->addEdge(rf, postreadfrom);
const ModelAction *postreadfrom = lastact->get_reads_from();
if (postreadfrom != NULL&&rf != postreadfrom)
mo_graph->addEdge(rf, postreadfrom);
- } else if (rf != lastact) {
- mo_graph->addEdge(rf, lastact);
+ } else {
+ //Case 3: The resolved read is a normal read and the next
+ //operation is a write, and we need to make sure that the
+ //write is mod ordered after rf
+ if (lastact!=rf)
+ mo_graph->addEdge(rf, lastact);
}
break;
}
}
break;
}