X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=3bac9039b4822475bb0226adcf4fd85cc8008ea1;hb=refs%2Fheads%2Fmaster;hp=089d88d11ca32c6a5cdaef4e41a4ed886285bf89;hpb=7bfea91f33595532cf618fe3d090e8021f578795;p=model-checker.git diff --git a/model.cc b/model.cc index 089d88d..3bac903 100644 --- a/model.cc +++ b/model.cc @@ -2,6 +2,7 @@ #include #include #include +#include #include "model.h" #include "action.h" @@ -16,30 +17,30 @@ #include "execution.h" #include "bugmessage.h" -#define INITIAL_THREAD_ID 0 - ModelChecker *model; /** @brief Constructor */ ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ params(params), + restart_flag(false), + exit_flag(false), scheduler(new Scheduler()), node_stack(new NodeStack()), - execution(new ModelExecution(this, ¶ms, scheduler, node_stack)), + execution(new ModelExecution(this, &this->params, scheduler, node_stack)), execution_number(1), diverge(NULL), earliest_diverge(NULL), - trace_analyses() + trace_analyses(), + inspect_plugin(NULL) { + memset(&stats,0,sizeof(struct execution_stats)); } /** @brief Destructor */ ModelChecker::~ModelChecker() { delete node_stack; - for (unsigned int i = 0; i < trace_analyses.size(); i++) - delete trace_analyses[i]; delete scheduler; } @@ -201,15 +202,13 @@ void ModelChecker::assert_user_bug(const char *msg) /** @brief Print bug report listing for this execution (if any bugs exist) */ void ModelChecker::print_bugs() const { - if (execution->have_bug_reports()) { - SnapVector *bugs = execution->get_bugs(); - - model_print("Bug report: %zu bug%s detected\n", - bugs->size(), - bugs->size() > 1 ? "s" : ""); - for (unsigned int i = 0; i < bugs->size(); i++) - (*bugs)[i]->print(); - } + SnapVector *bugs = execution->get_bugs(); + + model_print("Bug report: %zu bug%s detected\n", + bugs->size(), + bugs->size() > 1 ? "s" : ""); + for (unsigned int i = 0; i < bugs->size(); i++) + (*bugs)[i]->print(); } /** @@ -247,7 +246,8 @@ void ModelChecker::print_stats() const model_print("Number of buggy executions: %d\n", stats.num_buggy_executions); model_print("Number of infeasible executions: %d\n", stats.num_infeasible); model_print("Total executions: %d\n", stats.num_total); - model_print("Total nodes created: %d\n", node_stack->get_total_nodes()); + if (params.verbose) + model_print("Total nodes created: %d\n", node_stack->get_total_nodes()); } /** @@ -256,10 +256,12 @@ void ModelChecker::print_stats() const */ void ModelChecker::print_execution(bool printbugs) const { + model_print("Program output from execution %d:\n", + get_execution_number()); print_program_output(); - if (params.verbose) { - model_print("Earliest divergence point since last feasible execution:\n"); + if (params.verbose >= 3) { + model_print("\nEarliest divergence point since last feasible execution:\n"); if (earliest_diverge) earliest_diverge->print(); else @@ -270,8 +272,10 @@ void ModelChecker::print_execution(bool printbugs) const } /* Don't print invalid bugs */ - if (printbugs) + if (printbugs && execution->have_bug_reports()) { + model_print("\n"); print_bugs(); + } model_print("\n"); execution->print_summary(); @@ -299,12 +303,15 @@ bool ModelChecker::next_execution() checkDataRaces(); run_trace_analyses(); + } else if (inspect_plugin && !execution->is_complete_execution() && + (execution->too_many_steps())) { + inspect_plugin->analyze(execution->get_action_trace()); } record_stats(); /* Output */ - if (params.verbose || (complete && execution->have_bug_reports())) + if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports())) print_execution(complete); else clear_program_output(); @@ -312,6 +319,14 @@ bool ModelChecker::next_execution() if (complete) earliest_diverge = NULL; + if (restart_flag) { + do_restart(); + return true; + } + + if (exit_flag) + return false; + if ((diverge = execution->get_next_backtrack()) == NULL) return false; @@ -322,6 +337,9 @@ bool ModelChecker::next_execution() execution_number++; + if (params.maxexecutions != 0 && stats.num_complete >= params.maxexecutions) + return false; + reset_to_initial_state(); return true; } @@ -352,26 +370,6 @@ Thread * ModelChecker::get_thread(const ModelAction *act) const return execution->get_thread(act); } -/** - * @brief Check if a Thread is currently enabled - * @param t The Thread to check - * @return True if the Thread is currently enabled - */ -bool ModelChecker::is_enabled(Thread *t) const -{ - return scheduler->is_enabled(t); -} - -/** - * @brief Check if a Thread is currently enabled - * @param tid The ID of the Thread to check - * @return True if the Thread is currently enabled - */ -bool ModelChecker::is_enabled(thread_id_t tid) const -{ - return scheduler->is_enabled(tid); -} - /** * Switch from a model-checker context to a user-thread context. This is the * complement of ModelChecker::switch_to_master and must be called from the @@ -402,6 +400,9 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) Thread *old = thread_current(); scheduler->set_current_thread(NULL); ASSERT(!old->get_pending()); + if (inspect_plugin != NULL) { + inspect_plugin->inspectModelAction(act); + } old->set_pending(act); if (Thread::swap(old, &system_context) < 0) { perror("swap threads"); @@ -431,9 +432,35 @@ bool ModelChecker::should_terminate_execution() return false; } +/** @brief Exit ModelChecker upon returning to the run loop of the + * model checker. */ +void ModelChecker::exit_model_checker() +{ + exit_flag = true; +} + +/** @brief Restart ModelChecker upon returning to the run loop of the + * model checker. */ +void ModelChecker::restart() +{ + restart_flag = true; +} + +void ModelChecker::do_restart() +{ + restart_flag = false; + diverge = NULL; + earliest_diverge = NULL; + reset_to_initial_state(); + node_stack->full_reset(); + memset(&stats,0,sizeof(struct execution_stats)); + execution_number = 1; +} + /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { + bool has_next; do { thrd_t user_thread; Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); @@ -446,7 +473,7 @@ void ModelChecker::run() * thread which just took a step--plus the first step * for any newly-created thread */ - for (unsigned int i = 0; i < execution->get_num_threads(); i++) { + for (unsigned int i = 0; i < get_num_threads(); i++) { thread_id_t tid = int_to_id(i); Thread *thr = get_thread(tid); if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) { @@ -460,7 +487,7 @@ void ModelChecker::run() for (unsigned int i = 0; i < get_num_threads(); i++) { Thread *th = get_thread(int_to_id(i)); ModelAction *act = th->get_pending(); - if (act && is_enabled(th) && !execution->check_action_enabled(act)) { + if (act && execution->is_enabled(th) && !execution->check_action_enabled(act)) { scheduler->sleep(th); } } @@ -481,10 +508,24 @@ void ModelChecker::run() t = execution->take_step(curr); } while (!should_terminate_execution()); - } while (next_execution()); + has_next = next_execution(); + if (inspect_plugin != NULL && !has_next) { + inspect_plugin->actionAtModelCheckingFinish(); + // Check if the inpect plugin set the restart flag + if (restart_flag) { + model_print("******* Model-checking RESTART: *******\n"); + has_next = true; + do_restart(); + } + } + } while (has_next); execution->fixup_release_sequences(); model_print("******* Model-checking complete: *******\n"); print_stats(); + + /* Have the trace analyses dump their output. */ + for (unsigned int i = 0; i < trace_analyses.size(); i++) + trace_analyses[i]->finish(); }