model: release_seq synchronization generates mo_graph edge "work entries"

Now, when the synchronization for a ModelAction is updated while resolving
release sequences, the affected ModelAction(s) can be queued to the work_queue
for later processing (i.e., checking for mo_graph edge additions).

Note that the MOEdgeWorkEntry is not yet handled in the work_queue loop.

diff --git a/model.cc b/model.cc
index 7aed29b61c6e5ea2ef66235810d31a7de54257c4..c7a71ccdb2f541869ae61bd968e78c1523c35548 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -438,7 +438,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        break;
                }
                case WORK_CHECK_RELEASE_SEQ:
                        break;
                }
                case WORK_CHECK_RELEASE_SEQ:

-                       resolve_release_sequences(work.location);
+                       resolve_release_sequences(work.location, &work_queue);

                        break;
                case WORK_CHECK_MO_EDGES:
                        /** @todo Perform follow-up mo_graph checks */
                        break;
                case WORK_CHECK_MO_EDGES:
                        /** @todo Perform follow-up mo_graph checks */


@@ -936,9 +936,12 @@ void ModelChecker::get_release_seq_heads(ModelAction *act,
  *
  * @param location The location/object that should be checked for release
  * sequence resolutions
  *
  * @param location The location/object that should be checked for release
  * sequence resolutions

- * @return True if any updates occurred (new synchronization, new mo_graph edges)
+ * @param work_queue The work queue to which to add work items as they are
+ * generated
+ * @return True if any updates occurred (new synchronization, new mo_graph
+ * edges)

  */
  */

-bool ModelChecker::resolve_release_sequences(void *location)
+bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)

 {
        std::list<ModelAction *> *list;
        list = lazy_sync_with_release->getptr(location);
 {
        std::list<ModelAction *> *list;
        list = lazy_sync_with_release->getptr(location);


@@ -961,14 +964,18 @@ bool ModelChecker::resolve_release_sequences(void *location)
                }
 
                if (updated) {
                }
 
                if (updated) {

+                       /* Re-check act for mo_graph edges */
+                       work_queue->push_back(MOEdgeWorkEntry(act));
+

                        /* propagate synchronization to later actions */
                        action_list_t::reverse_iterator it = action_trace->rbegin();
                        while ((*it) != act) {
                                ModelAction *propagate = *it;
                        /* propagate synchronization to later actions */
                        action_list_t::reverse_iterator it = action_trace->rbegin();
                        while ((*it) != act) {
                                ModelAction *propagate = *it;

-                               if (act->happens_before(propagate))
-                                       /** @todo new mo_graph edges along with
-                                        * this synchronization? */
+                               if (act->happens_before(propagate)) {

                                        propagate->synchronize_with(act);
                                        propagate->synchronize_with(act);

+                                       /* Re-check 'propagate' for mo_graph edges */
+                                       work_queue->push_back(MOEdgeWorkEntry(propagate));
+                               }

                        }
                }
                if (complete) {
                        }
                }
                if (complete) {

diff --git a/model.h b/model.h
index cf1770b7720ed68789a0e3edd070620e65f08c69..3d3eba78db81ee8a2904c1e14ed37102e4c4a930 100644 (file)
--- a/model.h
+++ b/model.h
@@ -136,7 +136,7 @@ private:
        bool w_modification_order(ModelAction *curr);
        bool release_seq_head(const ModelAction *rf,
                        std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;
        bool w_modification_order(ModelAction *curr);
        bool release_seq_head(const ModelAction *rf,
                        std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;

-       bool resolve_release_sequences(void *location);
+       bool resolve_release_sequences(void *location, work_queue_t *work_queue);

 
        ModelAction *diverge;
 
 
        ModelAction *diverge;