/* Find X : is_read(X) && X --sb-> curr */
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
+ if (act == curr)
+ continue;
if (act->get_tid() != curr->get_tid())
continue;
/* Stop at the beginning of the thread */
rel_heads_list_t release_heads;
get_release_seq_heads(curr, act, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!act->synchronize_with(release_heads[i]))
+ if (!curr->synchronize_with(release_heads[i]))
set_bad_synchronization();
if (release_heads.size() != 0)
updated = true;
*act < *last_sc_fence_thread_local) {
mo_graph->addEdge(act, rf);
added = true;
+ break;
}
/* C++, Section 29.3 statement 4 */
else if (act->is_seqcst() && last_sc_fence_local &&
*act < *last_sc_fence_local) {
mo_graph->addEdge(act, rf);
added = true;
+ break;
}
/* C++, Section 29.3 statement 6 */
else if (last_sc_fence_thread_before &&
*act < *last_sc_fence_thread_before) {
mo_graph->addEdge(act, rf);
added = true;
+ break;
}
}
*act < *last_sc_fence_thread_before) {
mo_graph->addEdge(act, curr);
added = true;
+ break;
}
/*