From: Brian Norris <banorris@uci.edu>
Date: Fri, 22 Feb 2013 17:42:00 +0000 (-0800)
Subject: action: backtrack/sleep-sets for seq-cst fences
X-Git-Tag: oopsla2013~233
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=086fd3b2eae9320656cec2010c69dd70e4a0832a

action: backtrack/sleep-sets for seq-cst fences

We now backtrack (and wake up sleep-set actions) on all pairs of seq-cst
operations such that at least one of the operations is a write or fence.
---

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