From f47ffb576e8ff886cb4ee7a1feaf31b3137a975a Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 3 Dec 2012 16:00:33 -0800 Subject: [PATCH] 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. --- action.cc | 12 +++++++----- model.cc | 1 + 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/action.cc b/action.cc index 402ff50..3d46bd9 100644 --- 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 d6ebfe5..e92cd4b 100644 --- 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: { -- 2.34.1