model: assign "pending" return values in release_seq_heads()

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 59b9f0bcdf7450b6b91ad4e3f01523dbcae37b8e..e8b860c2c5058a0daf3f42ada4ba42d470a80b0e 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.
  * @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
  * 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
  */
  * @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())
 {
        /* 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 */
        };
        if (!rf) {
                /* read from future: need to settle this later */

+               pending->rf = NULL;

                return false; /* incomplete */
        }
 
                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));
 
 
        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)
        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 */
                        }
                                /* release --mo-> act --mo--> rf */
                                return true; /* complete */
                        }

+                       /* act may break release sequence */
+                       pending->writes.push_back(act);

                        certain = false;
                }
                if (!future_ordered)
                        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);
                release_heads->push_back(release);

+               pending->writes.clear();
+       } else {
+               pending->release = release;
+               pending->rf = rf;
+       }

        return certain;
 }
 
        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;
 
        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 {
                /* 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;
                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]))
                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]))