X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=39a7c2170f59fb0ac9b3a7d2160ecb80027283ff;hb=81ea453e58cbb85fddff3aa8919dfbc59c3140eb;hp=0665ff49b9762c0e9317d5688d21437f614535ca;hpb=7ba211ec7d1cacbaa3ef2027f1a0f534888f1708;p=model-checker.git diff --git a/model.cc b/model.cc index 0665ff4..39a7c21 100644 --- a/model.cc +++ b/model.cc @@ -12,6 +12,7 @@ #include "promise.h" #include "datarace.h" #include "mutex.h" +#include "threads.h" #define INITIAL_THREAD_ID 0 @@ -99,6 +100,12 @@ int ModelChecker::get_num_threads() return priv->next_thread_id; } +/** @return The currently executing Thread. */ +Thread * ModelChecker::get_current_thread() +{ + return scheduler->get_current_thread(); +} + /** @return a sequence number for a new ModelAction */ modelclock_t ModelChecker::get_next_seq_num() { @@ -139,6 +146,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) 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()) { @@ -158,8 +168,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) 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(); @@ -181,23 +195,27 @@ bool ModelChecker::next_execution() 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(); @@ -423,7 +441,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { 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; @@ -468,11 +486,11 @@ bool ModelChecker::process_write(ModelAction *curr) * (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: { @@ -489,7 +507,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) scheduler->sleep(waiting); } else { do_complete_join(curr); - synchronized = true; + updated = true; /* trigger rel-seq checks */ } break; } @@ -500,9 +518,10 @@ bool ModelChecker::process_thread_action(ModelAction *curr) 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: { @@ -513,7 +532,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } - return synchronized; + return updated; } /** @@ -540,6 +559,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) 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 */ @@ -612,7 +633,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) /* 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); } @@ -920,7 +941,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf } } 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; } @@ -1045,14 +1070,22 @@ bool ModelChecker::w_modification_order(ModelAction *curr) 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; } @@ -1069,8 +1102,12 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ 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) && @@ -1314,6 +1351,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } 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)); @@ -1465,6 +1504,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) //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 @@ -1598,6 +1638,34 @@ static void print_list(action_list_t *list) 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()); + 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()); + } + + thread_array[action->get_tid()]=action; + } + fprintf(file,"}\n"); + model_free(thread_array); + fclose(file); +} +#endif + void ModelChecker::print_summary() { printf("\n"); @@ -1610,6 +1678,8 @@ void ModelChecker::print_summary() char buffername[100]; sprintf(buffername, "exec%04u", num_executions); mo_graph->dumpGraphToFile(buffername); + sprintf(buffername, "graph%04u", num_executions); + dumpGraph(buffername); #endif if (!isfinalfeasible()) @@ -1638,12 +1708,35 @@ void ModelChecker::remove_thread(Thread *t) scheduler->remove_thread(t); } +/** + * @brief Get a Thread reference by its ID + * @param tid The Thread's ID + * @return A Thread reference + */ +Thread * ModelChecker::get_thread(thread_id_t tid) +{ + return thread_map->get(id_to_int(tid)); +} + +/** + * @brief Get a reference to the Thread in which a ModelAction was executed + * @param act The ModelAction + * @return A Thread reference + */ +Thread * ModelChecker::get_thread(ModelAction *act) +{ + return get_thread(act->get_tid()); +} + /** * Switch from a user-context to the "master thread" context (a.k.a. system * context). This switch is made with the intention of exploring a particular * model-checking action (described by a ModelAction object). Must be called * from a user-thread context. - * @param act The current action that will be explored. Must not be NULL. + * + * @param act The current action that will be explored. May be NULL only if + * trace is exiting via an assertion (see ModelChecker::set_assert and + * ModelChecker::has_asserted). * @return Return status from the 'swap' call (i.e., success/fail, 0/-1) */ int ModelChecker::switch_to_master(ModelAction *act)