model: release_seq synchronization generates mo_graph edge "work entries"

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 79c52d019d35f2ad39d22300597ee4575682f61d..c7a71ccdb2f541869ae61bd968e78c1523c35548 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -417,16 +417,36 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                break;
        }
 
-       bool updated = false;
+       work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
+
+       while (!work_queue.empty()) {
+               WorkQueueEntry work = work_queue.front();
+               work_queue.pop_front();
 
-       if (curr->is_read() && process_read(curr, second_part_of_rmw))
-               updated = true;
+               switch (work.type) {
+               case WORK_CHECK_CURR_ACTION: {
+                       ModelAction *act = work.action;
+                       bool updated = false;
+                       if (act->is_read() && process_read(act, second_part_of_rmw))
+                               updated = true;
 
-       if (curr->is_write() && process_write(curr))
-               updated = true;
+                       if (act->is_write() && process_write(act))
+                               updated = true;
 
-       if (updated)
-               resolve_release_sequences(curr->get_location());
+                       if (updated)
+                               work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
+                       break;
+               }
+               case WORK_CHECK_RELEASE_SEQ:
+                       resolve_release_sequences(work.location, &work_queue);
+                       break;
+               case WORK_CHECK_MO_EDGES:
+                       /** @todo Perform follow-up mo_graph checks */
+               default:
+                       ASSERT(false);
+                       break;
+               }
+       }
 
        /* Add action to list.  */
        if (!second_part_of_rmw)
@@ -916,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);
@@ -941,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) {