projects
/
c11tester.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model: release_seq_head: improve ordering of tests
[c11tester.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index d2fc366cc77d88521d583558aa50d9680df9305e..508f3b98284920860c9ce5eb4231b786b070b979 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-1124,8
+1124,6
@@
bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
for (rit = list->rbegin(); rit != list->rend(); rit++) {
const ModelAction *act = *rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
const ModelAction *act = *rit;
- if (!act->is_write())
- continue;
/* Reach synchronization -> this thread is complete */
if (act->happens_before(release))
break;
/* Reach synchronization -> this thread is complete */
if (act->happens_before(release))
break;
@@
-1134,6
+1132,10
@@
bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
continue;
}
continue;
}
+ /* Only writes can break release sequences */
+ if (!act->is_write())
+ continue;
+
/* Check modification order */
if (mo_graph->checkReachable(rf, act)) {
/* rf --mo--> act */
/* Check modification order */
if (mo_graph->checkReachable(rf, act)) {
/* rf --mo--> act */