model: add work queue loop

This commit does not change the actual computations performed yet. It only
prepares a loop structure in which we could perform many different Work items,
queueing them up as they are generated.

diff --git a/model.cc b/model.cc
index 79c52d019d35f2ad39d22300597ee4575682f61d..7aed29b61c6e5ea2ef66235810d31a7de54257c4 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);
+                       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)

diff --git a/model.h b/model.h
index 248e1648b7e431c30fe60927274d8ae29a5b3a7f..cf1770b7720ed68789a0e3edd070620e65f08c69 100644 (file)
--- a/model.h
+++ b/model.h
@@ -17,6 +17,7 @@
 #include "action.h"
 #include "clockvector.h"
 #include "hashtable.h"
+#include "workqueue.h"
 
 /* Forward declaration */
 class NodeStack;