X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=e3d9203eea60ec53010d67bb87da20331cfbf642;hb=af25bde59ce05189adee92825ecc03fbb83e675b;hp=0665ff49b9762c0e9317d5688d21437f614535ca;hpb=7ba211ec7d1cacbaa3ef2027f1a0f534888f1708;p=model-checker.git diff --git a/model.cc b/model.cc index 0665ff4..e3d9203 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,13 +168,17 @@ 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(); } - DEBUG("*** ModelChecker chose next thread = %d ***\n", tid); + DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid)); ASSERT(tid != THREAD_ID_T_NONE); return thread_map->get(id_to_int(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(); + 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(); @@ -306,7 +324,8 @@ void ModelChecker::set_backtracking(ModelAction *act) if (!node->set_backtrack(tid)) continue; DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n", - prev->get_tid(), t->get_id()); + id_to_int(prev->get_tid()), + id_to_int(t->get_id())); if (DBG_ENABLED()) { prev->print(); act->print(); @@ -423,7 +442,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 +487,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 +508,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 +519,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 +533,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } - return synchronized; + return updated; } /** @@ -540,6 +560,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 +634,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); } @@ -773,8 +795,7 @@ bool ModelChecker::isfinalfeasible() { /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ ModelAction * ModelChecker::process_rmw(ModelAction *act) { - int tid = id_to_int(act->get_tid()); - ModelAction *lastread = get_last_action(tid); + ModelAction *lastread = get_last_action(act->get_tid()); lastread->process_rmw(act); if (act->is_rmw() && lastread->get_reads_from()!=NULL) { mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); @@ -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) && @@ -1139,7 +1176,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * @return true, if the ModelChecker is certain that release_heads is complete; * false otherwise */ -bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const +bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const { /* Only check for release sequences if there are no cycles */ if (mo_graph->checkForCycles()) @@ -1209,7 +1246,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel ModelAction *last = get_last_action(int_to_id(i)); if (last && (rf->happens_before(last) || - last->get_type() == THREAD_FINISH)) + get_thread(int_to_id(i))->is_complete())) future_ordered = true; for (rit = list->rbegin(); rit != list->rend(); rit++) { @@ -1261,13 +1298,13 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel * @param act The 'acquire' action that may read from a release sequence * @param release_heads A pass-by-reference return parameter. Will be filled * with the head(s) of the release sequence(s), if they exists with certainty. - * @see ModelChecker::release_seq_head + * @see ModelChecker::release_seq_heads */ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) { const ModelAction *rf = act->get_reads_from(); bool complete; - complete = release_seq_head(rf, release_heads); + complete = release_seq_heads(rf, release_heads); if (!complete) { /* add act to 'lazy checking' list */ pending_acq_rel_seq->push_back(act); @@ -1303,7 +1340,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ const ModelAction *rf = act->get_reads_from(); rel_heads_list_t release_heads; bool complete; - complete = release_seq_head(rf, &release_heads); + complete = release_seq_heads(rf, &release_heads); for (unsigned int i = 0; i < release_heads.size(); i++) { if (!act->has_synchronized_with(release_heads[i])) { if (act->synchronize_with(release_heads[i])) @@ -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) const +{ + 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) const +{ + 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) @@ -1663,7 +1756,7 @@ bool ModelChecker::take_step() { if (has_asserted()) return false; - Thread * curr = thread_current(); + Thread *curr = thread_current(); if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); @@ -1677,22 +1770,23 @@ bool ModelChecker::take_step() { ASSERT(false); } } - Thread * next = scheduler->next_thread(priv->nextThread); + Thread *next = scheduler->next_thread(priv->nextThread); /* Infeasible -> don't take any more steps */ if (!isfeasible()) return false; - if (next) - next->set_state(THREAD_RUNNING); - DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1); + DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, + next ? id_to_int(next->get_id()) : -1); /* next == NULL -> don't take any more steps */ if (!next) return false; - if ( next->get_pending() != NULL ) { - //restart a pending action + next->set_state(THREAD_RUNNING); + + if (next->get_pending() != NULL) { + /* restart a pending action */ set_current_action(next->get_pending()); next->set_pending(NULL); next->set_state(THREAD_READY);