From 05f82cd6ab941db2d63ca83e778a430752de1900 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 20 Sep 2012 10:59:14 -0700 Subject: [PATCH] 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. --- model.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/model.cc b/model.cc index d2fc366..508f3b9 100644 --- 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; - if (!act->is_write()) - continue; /* 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; } + /* Only writes can break release sequences */ + if (!act->is_write()) + continue; + /* Check modification order */ if (mo_graph->checkReachable(rf, act)) { /* rf --mo--> act */ -- 2.34.1