model: rename release_seq_head() -> release_seq_heads()

It may return multiple heads, so make it plural.

diff --git a/model.cc b/model.cc
index 326358ea79c8b80ed0a356854cef43288c0ec304..21b2b77b16c83cced2f13730e8f0ac2e59bcc577 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1176,7 +1176,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * @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_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
+bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) 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())


@@ -1298,13 +1298,13 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
  * @param act The 'acquire' action that may read from a release sequence
  * @param release_heads A pass-by-reference return parameter. Will be filled
  * with the head(s) of the release sequence(s), if they exists with certainty.
  * @param act The 'acquire' action that may read from a release sequence
  * @param release_heads A pass-by-reference return parameter. Will be filled
  * with the head(s) of the release sequence(s), if they exists with certainty.

- * @see ModelChecker::release_seq_head
+ * @see ModelChecker::release_seq_heads

  */
 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
 {
        const ModelAction *rf = act->get_reads_from();
        bool complete;
  */
 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
 {
        const ModelAction *rf = act->get_reads_from();
        bool complete;

-       complete = release_seq_head(rf, release_heads);
+       complete = release_seq_heads(rf, release_heads);

        if (!complete) {
                /* add act to 'lazy checking' list */
                pending_acq_rel_seq->push_back(act);
        if (!complete) {
                /* add act to 'lazy checking' list */
                pending_acq_rel_seq->push_back(act);


@@ -1340,7 +1340,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_head(rf, &release_heads);
+               complete = release_seq_heads(rf, &release_heads);

                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 3dbd562755e41ece4f9836b9e6fa53a9c52c313f..d8dce07cbdf56423e04e2378d2e0715d18025559 100644 (file)
--- a/model.h
+++ b/model.h
@@ -148,7 +148,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_head(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+       bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) 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);