X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=a74147be4bbe7e068a9ddd05a58ff459ccb1a7c8;hb=3a4e118d45bf83a3b4c3a0a73d1071fa8fe5476d;hp=e962b92da41bb57193fc1bbcbf0b386514a35ec2;hpb=960e943616c59281fc10cd274ca04300d66c6391;p=model-checker.git

diff --git a/execution.cc b/execution.cc
index e962b92..a74147b 100644
--- a/execution.cc
+++ b/execution.cc
@@ -366,7 +366,10 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
 ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 {
 	switch (act->get_type()) {
-	/* case ATOMIC_FENCE: fences don't directly cause backtracking */
+	case ATOMIC_FENCE:
+		/* Only seq-cst fences can (directly) cause backtracking */
+		if (!act->is_seqcst())
+			break;
 	case ATOMIC_READ:
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {
@@ -377,6 +380,8 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
+			if (prev == act)
+				continue;
 			if (prev->could_synchronize_with(act)) {
 				ret = prev;
 				break;