execution: bugfix - backtrack seq-cst fences properly

[model-checker.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index e962b92da41bb57193fc1bbcbf0b386514a35ec2..fc2370616388d0c60acf8048fceee307e33ef269 100644 (file)
--- 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: {