model: release_seq_head: improve ordering of tests

We can get useful information from a non-write action, as long as we aren't
checking it for modification order or breaking of the release sequence.

diff --git a/model.cc b/model.cc
index d2fc366cc77d88521d583558aa50d9680df9305e..508f3b98284920860c9ce5eb4231b786b070b979 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1124,8 +1124,6 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        const ModelAction *act = *rit;
 
                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;
                        /* Reach synchronization -> this thread is complete */
                        if (act->happens_before(release))
                                break;


@@ -1134,6 +1132,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
                                continue;
                        }
 
                                continue;
                        }
 

+                       /* Only writes can break release sequences */
+                       if (!act->is_write())
+                               continue;
+

                        /* Check modification order */
                        if (mo_graph->checkReachable(rf, act)) {
                                /* rf --mo--> act */
                        /* Check modification order */
                        if (mo_graph->checkReachable(rf, act)) {
                                /* rf --mo--> act */