model: release_seq synchronization generates mo_graph edge "work entries"

[model-checker.git] / model.cc

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:
-                       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 */
@@ -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
- * @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);
@@ -961,14 +964,18 @@ bool ModelChecker::resolve_release_sequences(void *location)
                }
 
                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;
-                               if (act->happens_before(propagate))
-                                       /** @todo new mo_graph edges along with
-                                        * this synchronization? */
+                               if (act->happens_before(propagate)) {
                                        propagate->synchronize_with(act);
+                                       /* Re-check 'propagate' for mo_graph edges */
+                                       work_queue->push_back(MOEdgeWorkEntry(propagate));
+                               }
                        }
                }
                if (complete) {