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 33c862bac36fd2a7e788cfae00a1a46a774ecd4a..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: {
@@
-1209,7
+1212,7
@@
bool ModelExecution::check_action_enabled(ModelAction *curr) {
*
* @param curr The current action to process
* @return The ModelAction that is actually executed; may be different than
*
* @param curr The current action to process
* @return The ModelAction that is actually executed; may be different than
- * curr
; may be NULL, if the current action is not enabled to run
+ * curr
*/
ModelAction * ModelExecution::check_current_action(ModelAction *curr)
{
*/
ModelAction * ModelExecution::check_current_action(ModelAction *curr)
{