model: fix - RMW cannot break release sequences

I misinterpreted the spec's description of release sequences.

diff --git a/model.cc b/model.cc
index 2aaa1c26dbea3ad9e78720683635a117d83243f1..134e457eb44468e02c4d9879e89e1c25a1679c2a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1509,8 +1509,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
                                continue;
                        }
 
                                continue;
                        }
 

-                       /* Only writes can break release sequences */
-                       if (!act->is_write())
+                       /* Only non-RMW writes can break release sequences */
+                       if (!act->is_write() || act->is_rmw())

                                continue;
 
                        /* Check modification order */
                                continue;
 
                        /* Check modification order */