model: fix release_seq for open-ended synchronization

This fix handles the case where a thread may not yet have synchronized in a way
that ensures no future writes may break a release sequence. If we encounter
such a thread, we can return false (uncertain) and re-check this potential
release sequence later in the execution.

diff --git a/model.cc b/model.cc
index 37bddaf96dcfc9b4a16b5b2dd426ad395ed65327..e71947ddd5540f6e2db045deac77644e6a09a862 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -604,6 +604,11 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
                if (id_to_int(rf->get_tid()) == (int)i)
                        continue;
                list = &(*thrd_lists)[i];
+
+               /* Can we ensure no future writes from this thread may break
+                * the release seq? */
+               bool future_ordered = false;
+
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        const ModelAction *act = *rit;
                        if (!act->is_write())
@@ -611,13 +616,17 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
                        /* Reach synchronization -> this thread is complete */
                        if (act->happens_before(release))
                                break;
-                       if (rf->happens_before(act))
+                       if (rf->happens_before(act)) {
+                               future_ordered = true;
                                continue;
+                       }
 
                        /* Check modification order */
-                       if (mo_graph->checkReachable(rf, act))
+                       if (mo_graph->checkReachable(rf, act)) {
                                /* rf --mo--> act */
+                               future_ordered = true;
                                continue;
+                       }
                        if (mo_graph->checkReachable(act, release))
                                /* act --mo--> release */
                                break;
@@ -628,6 +637,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
                        }
                        certain = false;
                }
+               if (!future_ordered)
+                       return false; /* This thread is uncertain */
        }
 
        if (certain)