projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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()) {
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: {
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {