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

Now that the lazy pending release sequences list is improved, return
more information from release_seq_heads().

Note that this change also affects the behavior of the last double loop;
now, even after discovering write(s) from one thread that might break the
release sequence, I continue exploring other threads. This has some pros
and cons:

Con:
* may cause more work in exploring many threads without gaining any
  extra information

Pro:
* may help discover a write that *certainly* breaks the sequence,
  whereas previously, we might have exited with an uncertain status
* builds a more thorough, complete set of writes that might break the
  release sequence

The last point is the main intention, since we will require a complete
set for end-of-execution fixups. The others balance out to a net benefit
(and possibly a bugfix).

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]))

diff --git a/model.h b/model.h
index 6d892cbfeabeb92db267f1cc718b30972560371d..d5dc42266769004d542d72f472f6e1029c1a7e5c 100644 (file)
--- a/model.h
+++ b/model.h
@@ -163,7 +163,7 @@ private:
        void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
        bool r_modification_order(ModelAction *curr, const ModelAction *rf);
        bool w_modification_order(ModelAction *curr);
        void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
        bool r_modification_order(ModelAction *curr, const ModelAction *rf);
        bool w_modification_order(ModelAction *curr);

-       bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+       bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;

        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
        void do_complete_join(ModelAction *join);
 
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
        void do_complete_join(ModelAction *join);