X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=715a2584f36a1538528489d60f987142ad0f2a77;hb=84d0cd2f078f4cb15c318a0fef2515feab570375;hp=b73d31a579051c94cb909cac5d7e8330cde00ee0;hpb=ff05fa2d8214200766cf442b47e3a7e1356341f8;p=model-checker.git diff --git a/model.cc b/model.cc index b73d31a..715a258 100644 --- a/model.cc +++ b/model.cc @@ -1517,18 +1517,21 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf *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; } } @@ -1705,6 +1708,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) *act < *last_sc_fence_thread_before) { mo_graph->addEdge(act, curr); added = true; + break; } /*