From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Dec 2012 00:00:33 +0000 (-0800)
Subject: action/model: backtrack for seq-cst and release/acquire fences
X-Git-Tag: oopsla2013~483
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=f47ffb576e8ff886cb4ee7a1feaf31b3137a975a

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 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: {