model: release_seq_head: improve ordering of tests

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index a7c99af24b7b05633183e9f96494e873e9e3a5b3..508f3b98284920860c9ce5eb4231b786b070b979 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1118,10 +1118,12 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
                 * the release seq? */
                bool future_ordered = false;
 
+               ModelAction *last = get_last_action(int_to_id(i));
+               if (last && rf->happens_before(last))
+                       future_ordered = true;
+
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        const ModelAction *act = *rit;
-                       if (!act->is_write())
-                               continue;
                        /* Reach synchronization -> this thread is complete */
                        if (act->happens_before(release))
                                break;
@@ -1130,6 +1132,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
                                continue;
                        }
 
+                       /* Only writes can break release sequences */
+                       if (!act->is_write())
+                               continue;
+
                        /* Check modification order */
                        if (mo_graph->checkReachable(rf, act)) {
                                /* rf --mo--> act */