From 086fd3b2eae9320656cec2010c69dd70e4a0832a Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 22 Feb 2013 09:42:00 -0800 Subject: [PATCH] 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. --- action.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.34.1