action: backtrack/sleep-sets for seq-cst fences
authorBrian Norris <banorris@uci.edu>
Fri, 22 Feb 2013 17:42:00 +0000 (09:42 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 22 Feb 2013 17:43:42 +0000 (09:43 -0800)
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.

action.cc

index 317c6a7..2390ecc 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