ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
+ if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+ earliest_diverge=diverge;
+
Node *nextnode = next->get_node();
/* Reached divergence point */
if (nextnode->increment_promise()) {
Node *node = nextnode->get_parent();
tid = node->get_next_backtrack();
node_stack->pop_restofstack(1);
+ if (diverge==earliest_diverge) {
+ earliest_diverge=node->get_action();
+ }
}
DEBUG("*** Divergence point ***\n");
+
diverge = NULL;
} else {
tid = next->get_tid();
if ((diverge = get_next_backtrack()) == NULL)
return false;
- if (earliest_diverge == NULL || *diverge < *earliest_diverge)
- earliest_diverge=diverge;
-
if (DBG_ENABLED()) {
printf("Next execution will diverge at:\n");
diverge->print();
* (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
*
* @param curr The current action
- * @return True if synchronization was updated
+ * @return True if synchronization was updated or a thread completed
*/
bool ModelChecker::process_thread_action(ModelAction *curr)
{
- bool synchronized = false;
+ bool updated = false;
switch (curr->get_type()) {
case THREAD_CREATE: {
Thread *blocking = (Thread *)curr->get_location();
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
- synchronized = true;
+ updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_FINISH: {
scheduler->wake(get_thread(act));
}
th->complete();
+ updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
break;
}
- return synchronized;
+ return updated;
}
/**
return newcurr;
}
+ curr->set_seq_number(get_next_seq_num());
+
newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
if (newcurr) {
/* First restore type and order in case of RMW operation */