model: assign "pending" return values in release_seq_heads()
[model-checker.git] / model.cc
index 59b9f0b..e8b860c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1174,13 +1174,19 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * @todo Finish lazy updating, when promises are fulfilled in the future
  * @param rf The action that might be part of a release sequence. Must be a
  * write.
- * @param release_heads A pass-by-reference style return parameter.  After
+ * @param release_heads A pass-by-reference style return parameter. After
  * execution of this function, release_heads will contain the heads of all the
- * relevant release sequences, if any exists
+ * relevant release sequences, if any exists with certainty
+ * @param pending A pass-by-reference style return parameter which is only used
+ * when returning false (i.e., uncertain). Returns most information regarding
+ * an uncertain release sequence, including any write operations that might
+ * break the sequence.
  * @return true, if the ModelChecker is certain that release_heads is complete;
  * false otherwise
  */
-bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
+bool ModelChecker::release_seq_heads(const ModelAction *rf,
+               rel_heads_list_t *release_heads,
+               struct release_seq *pending) const
 {
        /* Only check for release sequences if there are no cycles */
        if (mo_graph->checkForCycles())
@@ -1209,6 +1215,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re
        };
        if (!rf) {
                /* read from future: need to settle this later */
+               pending->rf = NULL;
                return false; /* incomplete */
        }
 
@@ -1238,6 +1245,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re
 
        ASSERT(rf->same_thread(release));
 
+       pending->writes.clear();
+
        bool certain = true;
        for (unsigned int i = 0; i < thrd_lists->size(); i++) {
                if (id_to_int(rf->get_tid()) == (int)i)
@@ -1281,14 +1290,21 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re
                                /* release --mo-> act --mo--> rf */
                                return true; /* complete */
                        }
+                       /* act may break release sequence */
+                       pending->writes.push_back(act);
                        certain = false;
                }
                if (!future_ordered)
-                       return false; /* This thread is uncertain */
+                       certain = false; /* This thread is uncertain */
        }
 
-       if (certain)
+       if (certain) {
                release_heads->push_back(release);
+               pending->writes.clear();
+       } else {
+               pending->release = release;
+               pending->rf = rf;
+       }
        return certain;
 }
 
@@ -1310,7 +1326,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
        struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
        sequence->acquire = act;
 
-       if (!release_seq_heads(rf, release_heads)) {
+       if (!release_seq_heads(rf, release_heads, sequence)) {
                /* add act to 'lazy checking' list */
                pending_rel_seqs->push_back(sequence);
        } else {
@@ -1348,7 +1364,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                const ModelAction *rf = act->get_reads_from();
                rel_heads_list_t release_heads;
                bool complete;
-               complete = release_seq_heads(rf, &release_heads);
+               complete = release_seq_heads(rf, &release_heads, pending);
                for (unsigned int i = 0; i < release_heads.size(); i++) {
                        if (!act->has_synchronized_with(release_heads[i])) {
                                if (act->synchronize_with(release_heads[i]))