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 317c6a7cd87d9a94fbb695ecb95615ed5bae5613..2390ecc7bd39f115380172075d14cd9e1c56cbe8 100644 (file)
--- 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