From: Brian Norris <banorris@uci.edu>
Date: Wed, 17 Apr 2013 17:46:19 +0000 (-0700)
Subject: execution: bugfix - backtrack seq-cst fences properly
X-Git-Tag: oopsla2013~43
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=eb6e8431496fc3dfd7638fbfba4229f7215f6308

execution: bugfix - backtrack seq-cst fences properly

The commented-out ATOMIC_FENCE should not be commented out; the note
that "fences don't directly cause backtracking" is false for seq-cst
fences. We intend to backtrack for all seq-cst fences, so we need to
perform the appropriate 'get conflict' search for all fences.
---

diff --git a/execution.cc b/execution.cc
index e962b92..fc23706 100644
--- a/execution.cc
+++ b/execution.cc
@@ -366,7 +366,10 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
 ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 {
 	switch (act->get_type()) {
-	/* case ATOMIC_FENCE: fences don't directly cause backtracking */
+	case ATOMIC_FENCE:
+		/* Only seq-cst fences can (directly) cause backtracking */
+		if (!act->is_seqcst())
+			break;
 	case ATOMIC_READ:
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {