clockvector: add documentation

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 27b6cd6a9df24856be3c9b2cc712eb2972ae98f3..19d273de50bf67aa60cf6835845b21ac347fc7be 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
 
@@ -230,14 +231,28 @@ void ModelChecker::check_current_action(void)
        Node *currnode;
 
        ModelAction *curr = this->current_action;
+       ModelAction *tmp;
        current_action = NULL;
        if (!curr) {
                DEBUG("trying to push NULL action...\n");
                return;
        }
 
-       curr = node_stack->explore_action(curr);
-       curr->create_cv(get_parent_action(curr->get_tid()));
+       tmp = node_stack->explore_action(curr);
+       if (tmp) {
+               /* Discard duplicate ModelAction; use action from NodeStack */
+               delete curr;
+               curr = tmp;
+       } else {
+               /*
+                * Perform one-time actions when pushing new ModelAction onto
+                * NodeStack
+                */
+               curr->create_cv(get_parent_action(curr->get_tid()));
+               /* Build may_read_from set */
+               if (curr->is_read())
+                       build_reads_from_past(curr);
+       }
 
        /* Assign 'creation' parent */
        if (curr->get_type() == THREAD_CREATE) {
@@ -258,6 +273,12 @@ void ModelChecker::check_current_action(void)
        add_action_to_lists(curr);
 }
 
+
+/**
+ * Adds an action to the per-object, per-thread action vector.
+ * @param act is the ModelAction to add.
+ */
+
 void ModelChecker::add_action_to_lists(ModelAction *act)
 {
        action_trace->push_back(act);
@@ -286,6 +307,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");