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"
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;
}
curr->get_node()->add_read_from(act);
- /* Include at most one act that "happens before" curr */
- if (act->happens_before(curr))
+ /* 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);
}
static void print_list(action_list_t *list)