num_executions(0),
num_feasible_executions(0),
diverge(NULL),
+ earliest_diverge(NULL),
action_trace(new action_list_t()),
thread_map(new HashTable<int, Thread *, int>()),
obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
DBG();
num_executions++;
- if (isfinalfeasible())
+ if (isfinalfeasible()) {
+ printf("Earliest divergence point since last feasible execution:\n");
+ if (earliest_diverge)
+ earliest_diverge->print(false);
+ else
+ printf("(Not set)\n");
+
+ earliest_diverge = NULL;
num_feasible_executions++;
+ }
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;
break;
}
case THREAD_JOIN: {
- Thread *waiting, *blocking;
- waiting = get_thread(curr);
- blocking = (Thread *)curr->get_location();
- if (!blocking->is_complete()) {
- blocking->push_wait_list(curr);
- scheduler->sleep(waiting);
- } else {
- do_complete_join(curr);
- synchronized = true;
- }
+ Thread *blocking = (Thread *)curr->get_location();
+ ModelAction *act = get_last_action(blocking->get_id());
+ curr->synchronize_with(act);
+ synchronized = true;
break;
}
case THREAD_FINISH: {
Thread *th = get_thread(curr);
while (!th->wait_list_empty()) {
ModelAction *act = th->pop_wait_list();
- Thread *wake = get_thread(act);
- scheduler->wake(wake);
- do_complete_join(act);
- synchronized = true;
+ scheduler->wake(get_thread(act));
}
th->complete();
break;
/* 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()));
- }
+ /* Always compute new clock vector */
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
} else {
newcurr = curr;
+
+ /* Always compute new clock vector */
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
/*
* Perform one-time actions when pushing new ModelAction onto
* NodeStack
*/
- curr->create_cv(get_parent_action(curr->get_tid()));
- if (curr->is_write())
- compute_promises(curr);
+ if (newcurr->is_write())
+ compute_promises(newcurr);
}
return newcurr;
}
/**
- * This method checks whether a model action is enabled at the given point.
- * At this point, it checks whether a lock operation would be successful at this point.
- * If not, it puts the thread in a waiter list.
+ * @brief Check whether a model action is enabled.
+ *
+ * Checks whether a lock or join operation would be successful (i.e., is the
+ * lock already locked, or is the joined thread already complete). If not, put
+ * the action in a waiter list.
+ *
* @param curr is the ModelAction to check whether it is enabled.
* @return a bool that indicates whether the action is enabled.
*/
lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
return false;
}
+ } else if (curr->get_type() == THREAD_JOIN) {
+ Thread *blocking = (Thread *)curr->get_location();
+ if (!blocking->is_complete()) {
+ blocking->push_wait_list(curr);
+ return false;
+ }
}
return true;
if (!check_action_enabled(curr)) {
/* Make the execution look like we chose to run this action
- * much later, when a lock is actually available to release */
+ * much later, when a lock/join can succeed */
get_current_thread()->set_pending(curr);
- remove_thread(get_current_thread());
+ scheduler->sleep(get_current_thread());
return get_next_thread(NULL);
}
bool updated = false;
if (act->is_read()) {
- if (r_modification_order(act, act->get_reads_from()))
+ const ModelAction *rf = act->get_reads_from();
+ if (rf != NULL && r_modification_order(act, rf))
updated = true;
}
if (act->is_write()) {
return get_next_thread(curr);
}
-/**
- * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
- * operation from the Thread it is joining with. Must be called after the
- * completion of the Thread in question.
- * @param join The THREAD_JOIN action
- */
-void ModelChecker::do_complete_join(ModelAction *join)
-{
- Thread *blocking = (Thread *)join->get_location();
- ModelAction *act = get_last_action(blocking->get_id());
- join->synchronize_with(act);
-}
-
void ModelChecker::check_curr_backtracking(ModelAction * curr) {
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
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;
}
printf("---------------------------------------------------------------------\n");
}
+#if SUPPORT_MOD_ORDER_DUMP
+void ModelChecker::dumpGraph(char *filename) {
+ char buffer[200];
+ sprintf(buffer, "%s.dot",filename);
+ FILE *file=fopen(buffer, "w");
+ fprintf(file, "digraph %s {\n",filename);
+ mo_graph->dumpNodes(file);
+ ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
+
+ for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
+ 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 (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());
+ }
+
+ thread_array[action->get_tid()]=action;
+ }
+ fprintf(file,"}\n");
+ model_free(thread_array);
+ fclose(file);
+}
+#endif
+
void ModelChecker::print_summary()
{
printf("\n");
char buffername[100];
sprintf(buffername, "exec%04u", num_executions);
mo_graph->dumpGraphToFile(buffername);
+ sprintf(buffername, "graph%04u", num_executions);
+ dumpGraph(buffername);
#endif
if (!isfinalfeasible())