ModelAction *last_sc_write = NULL;
- /* Track whether this object has been initialized */
- bool initialized = false;
-
- if (curr->is_seqcst()) {
+ if (curr->is_seqcst())
last_sc_write = get_last_seq_cst_write(curr);
- /* We have to at least see the last sequentially consistent write,
- so we are initialized. */
- if (last_sc_write != NULL)
- initialized = true;
- }
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
}
/* Include at most one act per-thread that "happens before" curr */
- if (act->happens_before(curr)) {
- initialized = true;
+ if (act->happens_before(curr))
break;
- }
}
}
- if (!initialized)
- assert_bug("May read from uninitialized atomic");
-
- if (DBG_ENABLED() || !initialized) {
+ if (DBG_ENABLED()) {
model_print("Reached read action:\n");
curr->print();
model_print("Printing may_read_from\n");
}
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
- while(true) {
+ while (true) {
+ /* UNINIT actions don't have a Node, and they never sleep */
+ if (write->is_uninitialized())
+ return true;
Node *prevnode=write->get_node()->get_parent();
bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;