X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=2390ecc7bd39f115380172075d14cd9e1c56cbe8;hb=086fd3b2eae9320656cec2010c69dd70e4a0832a;hp=317c6a7cd87d9a94fbb695ecb95615ed5bae5613;hpb=d5ec9d02d3ce4a92811a4515f808efcb0a1326b7;p=model-checker.git

diff --git a/action.cc b/action.cc
index 317c6a7..2390ecc 100644
--- a/action.cc
+++ b/action.cc
@@ -300,9 +300,9 @@ bool ModelAction::could_synchronize_with(const ModelAction *act) const
 	if (!same_var(act))
 		return false;
 
-	// Explore interleavings of seqcst writes to guarantee total
+	// Explore interleavings of seqcst writes/fences to guarantee total
 	// order of seq_cst operations that don't commute
-	if ((could_be_write() || act->could_be_write()) && is_seqcst() && act->is_seqcst())
+	if ((could_be_write() || act->could_be_write() || is_fence() || act->is_fence()) && is_seqcst() && act->is_seqcst())
 		return true;
 
 	// Explore synchronizing read/write pairs