if (curr->is_rmwc() || curr->is_rmw()) {
newcurr = process_rmw(curr);
delete curr;
- compute_promises(newcurr);
+
+ if (newcurr->is_rmw())
+ compute_promises(newcurr);
return newcurr;
}
/* Discard duplicate ModelAction; use action from NodeStack */
delete curr;
- /* If we have diverged, we need to reset the clock vector. */
- if (diverge == NULL)
- newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
} else {
newcurr = curr;
/*
action_list_t::reverse_iterator rit;
ModelAction *lastact = NULL;
- /* Find last action that happens after curr */
+ /* Find last action that happens after curr that is either not curr or a rmw */
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (curr->happens_before(act)) {
+ if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
lastact = act;
} else
break;
/* Include at most one act per-thread that "happens before" curr */
if (lastact != NULL) {
- if (lastact->is_read()) {
+ if (lastact==curr) {
+ //Case 1: The resolved read is a RMW, and we need to make sure
+ //that the write portion of the RMW mod order after rf
+
+ mo_graph->addEdge(rf, lastact);
+ } else if (lastact->is_read()) {
+ //Case 2: The resolved read is a normal read and the next
+ //operation is a read, and we need to make sure the value read
+ //is mod ordered after rf
+
const ModelAction *postreadfrom = lastact->get_reads_from();
if (postreadfrom != NULL&&rf != postreadfrom)
mo_graph->addEdge(rf, postreadfrom);
- } else if (rf != lastact) {
- mo_graph->addEdge(rf, lastact);
+ } else {
+ //Case 3: The resolved read is a normal read and the next
+ //operation is a write, and we need to make sure that the
+ //write is mod ordered after rf
+ if (lastact!=rf)
+ mo_graph->addEdge(rf, lastact);
}
break;
}
complete = release_seq_head(rf, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++) {
if (!act->has_synchronized_with(release_heads[i])) {
- updated = true;
- act->synchronize_with(release_heads[i]);
+ if (act->synchronize_with(release_heads[i]))
+ updated = true;
+ else
+ set_bad_synchronization();
}
}
//Next fix up the modification order for actions that happened
//after the read.
post_r_modification_order(read, write);
+ //Make sure the promise's value matches the write's value
+ ASSERT(promise->get_value() == write->get_value());
promises->erase(promises->begin() + promise_index);
resolved = true;
priv->nextThread = check_current_action(priv->current_action);
priv->current_action = NULL;
+
if (curr->is_blocked() || curr->is_complete())
scheduler->remove_thread(curr);
} else {