+
+ 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) {
+ Thread *th = (Thread *)curr->get_location();
+ th->set_creation(curr);
+ }
+
+ nextThread = get_next_replay_thread();
+
+ currnode = curr->get_node()->get_parent();
+
+ if (!currnode->backtrack_empty())
+ if (!next_backtrack || *curr > *next_backtrack)
+ next_backtrack = curr;
+
+ set_backtracking(curr);
+
+ add_action_to_lists(curr);
+}
+
+/**
+ * Performs various bookkeeping operations for the current ModelAction. For
+ * instance, adds action to the per-object, per-thread action vector and to the
+ * action trace list of all thread actions.
+ *
+ * @param act is the ModelAction to add.
+ */
+void ModelChecker::add_action_to_lists(ModelAction *act)
+{
+ action_trace->push_back(act);
+
+ std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
+ if (id_to_int(act->get_tid()) >= (int)vec->size())
+ vec->resize(next_thread_id);
+ (*vec)[id_to_int(act->get_tid())].push_back(act);
+
+ (*thrd_last_action)[id_to_int(act->get_tid())] = act;
+}
+
+ModelAction * ModelChecker::get_last_action(thread_id_t tid)
+{
+ int nthreads = get_num_threads();
+ if ((int)thrd_last_action->size() < nthreads)
+ thrd_last_action->resize(nthreads);
+ return (*thrd_last_action)[id_to_int(tid)];
+}
+
+ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
+{
+ ModelAction *parent = get_last_action(tid);
+ if (!parent)
+ parent = get_thread(tid)->get_creation();
+ return parent;
+}
+
+ClockVector * ModelChecker::get_cv(thread_id_t tid) {
+ return get_parent_action(tid)->get_cv();
+}
+
+/**
+ * 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());
+
+ /* Track whether this object has been initialized */
+ bool initialized = false;
+
+ 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 per-thread that "happens before" curr */
+ if (act->happens_before(curr)) {
+ initialized = true;
+ break;
+ }
+ }
+ }
+
+ if (!initialized) {
+ /* TODO: need a more informative way of reporting errors */
+ printf("ERROR: may read from uninitialized atomic\n");
+ }
+
+ if (DBG_ENABLED() || !initialized) {
+ printf("Reached read action:\n");
+ curr->print();
+ printf("Printing may_read_from\n");
+ curr->get_node()->print_may_read_from();
+ printf("End printing may_read_from\n");
+ }
+
+ ASSERT(initialized);