action/model: backtrack for seq-cst and release/acquire fences

Extends backtracking support to explore all interleavings of conflicting
seq-cst fences and potentially-synchronizing write/read/fence pairs.

diff --git a/action.cc b/action.cc
index 402ff5064ace78cc8e2076aa7254e905063fc3bc..3d46bd91aa0de6a2dd1a5729a1867fd3737343b3 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -253,13 +253,15 @@ bool ModelAction::could_synchronize_with(const ModelAction *act) const
        if (!same_var(act))
                return false;
 
-       // Explore interleavings of seqcst writes 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())
+       // 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_fence() || act->is_fence())
+                       && is_seqcst() && act->is_seqcst())
                return true;
 
-       // Explore synchronizing read/write pairs
-       if (is_read() && is_acquire() && act->could_be_write() && act->is_release())
+       // Explore synchronizing read/write/fence pairs
+       if (is_acquire() && act->is_release() && (is_read() || is_fence()) &&
+                       (act->could_be_write() || act->is_fence()))
                return true;
 
        //lock just released...we can grab lock

diff --git a/model.cc b/model.cc
index d6ebfe5abc9f4e60920f9b08bed0112746c3afce..e92cd4b32e3bcc77e8f2389f03f89108ab97537d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -521,6 +521,7 @@ bool ModelChecker::next_execution()
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
        switch (act->get_type()) {
+       case ATOMIC_FENCE:
        case ATOMIC_READ:
        case ATOMIC_WRITE:
        case ATOMIC_RMW: {