X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=715a2584f36a1538528489d60f987142ad0f2a77;hb=84d0cd2f078f4cb15c318a0fef2515feab570375;hp=6120f4d4d688d908fb66c47b848b3db472c9081b;hpb=53f0d3f9d56fd6341ef725ce8651661d6d9d906e;p=model-checker.git

diff --git a/model.cc b/model.cc
index 6120f4d..715a258 100644
--- a/model.cc
+++ b/model.cc
@@ -879,6 +879,8 @@ bool ModelChecker::process_fence(ModelAction *curr)
 		/* 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 */
@@ -897,7 +899,7 @@ bool ModelChecker::process_fence(ModelAction *curr)
 			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;
@@ -1515,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;
 				}
 			}
 
@@ -1703,6 +1708,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 					*act < *last_sc_fence_thread_before) {
 				mo_graph->addEdge(act, curr);
 				added = true;
+				break;
 			}
 
 			/*