X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=c01122191d0e712750b382f87b9c0edbfecf9aa2;hp=0665ff49b9762c0e9317d5688d21437f614535ca;hb=61db3a1768f1b90ad997e648a7e622c7ef47b69b;hpb=7ba211ec7d1cacbaa3ef2027f1a0f534888f1708 diff --git a/model.cc b/model.cc index 0665ff4..c011221 100644 --- a/model.cc +++ b/model.cc @@ -139,6 +139,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 +161,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 +188,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 +434,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 +479,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 +500,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 +511,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 +525,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } - return synchronized; + return updated; } /** @@ -540,6 +552,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 +626,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); } @@ -1314,6 +1328,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 +1481,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 +1615,33 @@ 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()); + 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 +1654,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())