model: add build_reads_from_past() function

Add function that will build up the initial set of all past writes that a
'read' action may read from.

diff --git a/model.cc b/model.cc
index 077cc53ea9cd252365214cb2a424a0da8476002b..e4d3016e0eeaa9cfdec58d5c57f4cf0ba2dadbe8 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -6,6 +6,7 @@
 #include "schedule.h"
 #include "snapshot-interface.h"
 #include "common.h"
+#include "clockvector.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -299,6 +300,44 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
        return parent;
 }
 
+/**
+ * Build up an initial set of all past writes that this 'read' action may read
+ * from. This set is determined by the clock vector's "happens before"
+ * relationship.
+ * @param curr is the current ModelAction that we are exploring; it must be a
+ * 'read' operation.
+ */
+void ModelChecker::build_reads_from_past(ModelAction *curr)
+{
+       std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+       unsigned int i;
+
+       ASSERT(curr->is_read());
+
+       for (i = 0; i < thrd_lists->size(); i++) {
+               action_list_t *list = &(*thrd_lists)[i];
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *act = *rit;
+
+                       /* Only consider 'write' actions */
+                       if (!act->is_write())
+                               continue;
+
+                       DEBUG("Adding action to may_read_from:\n");
+                       if (DBG_ENABLED()) {
+                               act->print();
+                               curr->print();
+                       }
+                       curr->get_node()->add_read_from(act);
+
+                       /* Include at most one act that "happens before" curr */
+                       if (act->happens_before(curr))
+                               break;
+               }
+       }
+}
+
 void ModelChecker::print_summary(void)
 {
        printf("\n");

diff --git a/model.h b/model.h
index 8d79eb56a43ef36fe02dfc5ec4b6463f719b0126..ab961f840b03613492a4da2b8585453bbe6b2847 100644 (file)
--- a/model.h
+++ b/model.h
@@ -78,6 +78,7 @@ private:
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid);
        ModelAction * get_parent_action(thread_id_t tid);
+       void build_reads_from_past(ModelAction *curr);
 
        void print_list(action_list_t *list);