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();
DBG();
num_executions++;
+
if (isfinalfeasible()) {
printf("Earliest divergence point since last feasible execution:\n");
- earliest_diverge->print();
+ if (earliest_diverge)
+ earliest_diverge->print(false);
+ else
+ printf("(Not set)\n");
earliest_diverge = NULL;
num_feasible_executions++;
}
+ DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+ pending_acq_rel_seq->size());
+
if (isfinalfeasible() || DBG_ENABLED())
print_summary();
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();
action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
- scheduler->add_thread(get_thread((*rit)->get_tid()));
+ scheduler->wake(get_thread(*rit));
}
waiters->clear();
break;
* (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: {
scheduler->sleep(waiting);
} else {
do_complete_join(curr);
- synchronized = true;
+ updated = true; /* trigger rel-seq checks */
}
break;
}
Thread *wake = get_thread(act);
scheduler->wake(wake);
do_complete_join(act);
- synchronized = true;
+ updated = true; /* trigger rel-seq checks */
}
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 */
/* Make the execution look like we chose to run this action
* much later, when a lock is actually available to release */
get_current_thread()->set_pending(curr);
- remove_thread(get_current_thread());
+ scheduler->sleep(get_current_thread());
return get_next_thread(NULL);
}
}
} else {
const ModelAction *prevreadfrom = act->get_reads_from();
- if (prevreadfrom != NULL && rf != prevreadfrom) {
+ //if the previous read is unresolved, keep going...
+ if (prevreadfrom == NULL)
+ continue;
+
+ if (rf != prevreadfrom) {
mo_graph->addEdge(prevreadfrom, rf);
added = true;
}
ModelAction *act = *rit;
if (act == curr) {
/*
- * If RMW, we already have all relevant edges,
- * so just skip to next thread.
- * If normal write, we need to look at earlier
- * actions, so continue processing list.
+ * 1) If RMW and it actually read from something, then we
+ * already have all relevant edges, so just skip to next
+ * thread.
+ *
+ * 2) If RMW and it didn't read from anything, we should
+ * whatever edge we can get to speed up convergence.
+ *
+ * 3) If normal write, we need to look at earlier actions, so
+ * continue processing list.
*/
- if (curr->is_rmw())
- break;
- else
+ if (curr->is_rmw()) {
+ if (curr->get_reads_from()!=NULL)
+ break;
+ else
+ continue;
+ } else
continue;
}
*/
if (act->is_write())
mo_graph->addEdge(act, curr);
- else if (act->is_read() && act->get_reads_from() != NULL)
+ else if (act->is_read()) {
+ //if previous read accessed a null, just keep going
+ if (act->get_reads_from() == NULL)
+ continue;
mo_graph->addEdge(act->get_reads_from(), curr);
+ }
added = true;
break;
} else if (act->is_read() && !act->is_synchronizing(curr) &&
}
if (updated) {
+ /* Re-check all pending release sequences */
+ work_queue->push_back(CheckRelSeqWorkEntry(NULL));
/* Re-check act for mo_graph edges */
work_queue->push_back(MOEdgeWorkEntry(act));
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
+ delete(promise);
promises->erase(promises->begin() + promise_index);
resolved = true;
} else
ModelAction *action=*it;
if (action->is_read()) {
fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
- fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+ if (action->get_reads_from()!=NULL)
+ fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
}
if (thread_array[action->get_tid()] != NULL) {
fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());