X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=f1df6ae8bfbbdacd806f56976de6b1c2f2bc8099;hp=8e94561531ca063ccbd23bec2bf51d778530a95d;hb=e45f16f22c8e36652a8f11f6f085ac43da24e1a8;hpb=634ad19a6e82ddefd9c30d01523fc7fb42540c4c diff --git a/model.cc b/model.cc index 8e945615..f1df6ae8 100644 --- a/model.cc +++ b/model.cc @@ -2,10 +2,11 @@ #include #include #include +#include +#include #include "model.h" #include "action.h" -#include "nodestack.h" #include "schedule.h" #include "snapshot-interface.h" #include "common.h" @@ -14,51 +15,106 @@ #include "output.h" #include "traceanalysis.h" #include "execution.h" +#include "history.h" #include "bugmessage.h" +#include "params.h" +#include "plugins.h" -ModelChecker *model; +ModelChecker *model = NULL; + +void placeholder(void *) { + ASSERT(0); +} + +#include + +#define SIGSTACKSIZE 65536 +static void mprot_handle_pf(int sig, siginfo_t *si, void *unused) +{ + model_print("Segmentation fault at %p\n", si->si_addr); + model_print("For debugging, place breakpoint at: %s:%d\n", + __FILE__, __LINE__); + print_trace(); // Trace printing may cause dynamic memory allocation + while(1) + ; +} + +void install_handler() { + stack_t ss; + ss.ss_sp = model_malloc(SIGSTACKSIZE); + ss.ss_size = SIGSTACKSIZE; + ss.ss_flags = 0; + sigaltstack(&ss, NULL); + struct sigaction sa; + sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK; + sigemptyset(&sa.sa_mask); + sa.sa_sigaction = mprot_handle_pf; + + if (sigaction(SIGSEGV, &sa, NULL) == -1) { + perror("sigaction(SIGSEGV)"); + exit(EXIT_FAILURE); + } + +} /** @brief Constructor */ -ModelChecker::ModelChecker(struct model_params params) : +ModelChecker::ModelChecker() : /* Initialize default scheduler */ - params(params), + params(), scheduler(new Scheduler()), - node_stack(new NodeStack()), - execution(new ModelExecution(this, ¶ms, scheduler, node_stack)), + history(new ModelHistory()), + execution(new ModelExecution(this, scheduler)), execution_number(1), - diverge(NULL), - earliest_diverge(NULL), - trace_analyses() + trace_analyses(), + inspect_plugin(NULL) { + model_print("C11Tester\n" + "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n" + "Distributed under the GPLv2\n" + "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n"); + memset(&stats,0,sizeof(struct execution_stats)); + init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &placeholder, NULL, NULL); +#ifdef TLS + init_thread->setTLS((char *)get_tls_addr()); +#endif + execution->add_thread(init_thread); + scheduler->set_current_thread(init_thread); + register_plugins(); + execution->setParams(¶ms); + param_defaults(¶ms); + parse_options(¶ms); + initRaceDetector(); + /* Configure output redirection for the model-checker */ + install_handler(); } /** @brief Destructor */ ModelChecker::~ModelChecker() { - delete node_stack; - for (unsigned int i = 0; i < trace_analyses.size(); i++) - delete trace_analyses[i]; delete scheduler; } +/** Method to set parameters */ +model_params * ModelChecker::getParams() { + return ¶ms; +} + /** * Restores user program to initial state and resets all model-checker data * structures. */ void ModelChecker::reset_to_initial_state() { - DEBUG("+++ Resetting to initial state +++\n"); - node_stack->reset_execution(); /** * FIXME: if we utilize partial rollback, we will need to free only * those pending actions which were NOT pending before the rollback * point */ - for (unsigned int i = 0; i < get_num_threads(); i++) + for (unsigned int i = 0;i < get_num_threads();i++) delete get_thread(int_to_id(i))->get_pending(); - snapshot_backtrack_before(0); + snapshot_roll_back(snapshot); } /** @return the number of user threads created during this execution */ @@ -91,73 +147,12 @@ Thread * ModelChecker::get_current_thread() const */ Thread * ModelChecker::get_next_thread() { - thread_id_t tid; /* * Have we completed exploring the preselected path? Then let the * scheduler decide */ - if (diverge == NULL) - return scheduler->select_next_thread(node_stack->get_head()); - - - /* Else, we are trying to replay an execution */ - 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(); - Node *prevnode = nextnode->get_parent(); - scheduler->update_sleep_set(prevnode); - - /* Reached divergence point */ - if (nextnode->increment_behaviors()) { - /* Execute the same thread with a new behavior */ - tid = next->get_tid(); - node_stack->pop_restofstack(2); - } else { - ASSERT(prevnode); - /* Make a different thread execute for next step */ - scheduler->add_sleep(get_thread(next->get_tid())); - tid = prevnode->get_next_backtrack(); - /* Make sure the backtracked thread isn't sleeping. */ - node_stack->pop_restofstack(1); - if (diverge == earliest_diverge) { - earliest_diverge = prevnode->get_action(); - } - } - /* Start the round robin scheduler from this thread id */ - scheduler->set_scheduler_thread(tid); - /* The correct sleep set is in the parent node. */ - execute_sleep_set(); - - DEBUG("*** Divergence point ***\n"); - - diverge = NULL; - } else { - tid = next->get_tid(); - } - DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid)); - ASSERT(tid != THREAD_ID_T_NONE); - return get_thread(id_to_int(tid)); -} - -/** - * We need to know what the next actions of all threads in the sleep - * set will be. This method computes them and stores the actions at - * the corresponding thread object's pending action. - */ -void ModelChecker::execute_sleep_set() -{ - for (unsigned int i = 0; i < get_num_threads(); i++) { - thread_id_t tid = int_to_id(i); - Thread *thr = get_thread(tid); - if (scheduler->is_sleep_set(thr) && thr->get_pending()) { - thr->get_pending()->set_sleep_flag(); - } - } + return scheduler->select_next_thread(); } /** @@ -172,7 +167,7 @@ void ModelChecker::execute_sleep_set() * @param msg Descriptive message for the bug (do not include newline char) * @return True if bug is immediately-feasible */ -bool ModelChecker::assert_bug(const char *msg, ...) +void ModelChecker::assert_bug(const char *msg, ...) { char str[800]; @@ -181,7 +176,7 @@ bool ModelChecker::assert_bug(const char *msg, ...) vsnprintf(str, sizeof(str), msg, ap); va_end(ap); - return execution->assert_bug(str); + execution->assert_bug(str); } /** @@ -192,22 +187,20 @@ bool ModelChecker::assert_bug(const char *msg, ...) void ModelChecker::assert_user_bug(const char *msg) { /* If feasible bug, bail out now */ - if (assert_bug(msg)) - switch_to_master(NULL); + assert_bug(msg); + switch_to_master(NULL); } /** @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(); + 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(); - } + 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(); } /** @@ -218,16 +211,13 @@ void ModelChecker::print_bugs() const */ void ModelChecker::record_stats() { - stats.num_total++; - if (!execution->isfeasibleprefix()) - stats.num_infeasible++; - else if (execution->have_bug_reports()) - stats.num_buggy_executions++; + stats.num_total ++; + if (execution->have_bug_reports()) + stats.num_buggy_executions ++; else if (execution->is_complete_execution()) - stats.num_complete++; + stats.num_complete ++; else { - stats.num_redundant++; - + //All threads are sleeping /** * @todo We can violate this ASSERT() when fairness/sleep sets * conflict to cause an execution to terminate, e.g. with: @@ -241,11 +231,8 @@ void ModelChecker::record_stats() void ModelChecker::print_stats() const { model_print("Number of complete, bug-free executions: %d\n", stats.num_complete); - model_print("Number of redundant executions: %d\n", stats.num_redundant); 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()); } /** @@ -254,22 +241,19 @@ 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 (earliest_diverge) - earliest_diverge->print(); - else - model_print("(Not set)\n"); - - model_print("\n"); + if (params.verbose >= 3) { print_stats(); } /* Don't print invalid bugs */ - if (printbugs) + if (printbugs && execution->have_bug_reports()) { + model_print("\n"); print_bugs(); + } model_print("\n"); execution->print_summary(); @@ -282,52 +266,40 @@ void ModelChecker::print_execution(bool printbugs) const * @return If there are more executions to explore, return true. Otherwise, * return false. */ -bool ModelChecker::next_execution() +void ModelChecker::finish_execution(bool more_executions) { DBG(); /* Is this execution a feasible execution that's worth bug-checking? */ - bool complete = execution->isfeasibleprefix() && - (execution->is_complete_execution() || - execution->have_bug_reports()); + bool complete = (execution->is_complete_execution() || + execution->have_bug_reports()); /* End-of-execution bug checks */ if (complete) { if (execution->is_deadlocked()) assert_bug("Deadlock detected"); - checkDataRaces(); run_trace_analyses(); } 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(); - if (complete) - earliest_diverge = NULL; +// test code + execution_number ++; + if (more_executions) + reset_to_initial_state(); - if ((diverge = execution->get_next_backtrack()) == NULL) - return false; - - if (DBG_ENABLED()) { - model_print("Next execution will diverge at:\n"); - diverge->print(); - } - - execution_number++; - - reset_to_initial_state(); - return true; + history->set_new_exec_flag(); } /** @brief Run trace analyses on complete trace */ void ModelChecker::run_trace_analyses() { - for (unsigned int i = 0; i < trace_analyses.size(); i++) - trace_analyses[i]->analyze(execution->get_action_trace()); + for (unsigned int i = 0;i < trace_analyses.size();i ++) + trace_analyses[i] -> analyze(execution->get_action_trace()); } /** @@ -350,26 +322,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 @@ -396,10 +348,25 @@ void ModelChecker::switch_from_master(Thread *thread) */ uint64_t ModelChecker::switch_to_master(ModelAction *act) { + if (modellock) { + static bool fork_message_printed = false; + + if (!fork_message_printed) { + model_print("Fork handler or dead thread trying to call into model checker...\n"); + fork_message_printed = true; + } + delete act; + return 0; + } DBG(); 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"); @@ -408,43 +375,57 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) return old->get_return_value(); } -/** Wrapper to run the user's main function, with appropriate arguments */ -void user_main_wrapper(void *) -{ - user_main(model->params.argc, model->params.argv); +static void runChecker() { + model->run(); + delete model; +} + +void ModelChecker::startChecker() { + startExecution(get_system_context(), runChecker); + snapshot = take_snapshot(); + + install_trace_analyses(get_execution()); + redirect_output(); + initMainThread(); } bool ModelChecker::should_terminate_execution() { - /* Infeasible -> don't take any more steps */ - if (execution->is_infeasible()) - return true; - else if (execution->isfeasibleprefix() && execution->have_bug_reports()) { + if (execution->have_bug_reports()) { execution->set_assert(); return true; - } - - if (execution->too_many_steps()) + } else if (execution->isFinished()) { return true; + } return false; } /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { - do { - thrd_t user_thread; - Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); - execution->add_thread(t); + //Need to initial random number generator state to avoid resets on rollback + char random_state[256]; + initstate(423121, random_state, sizeof(random_state)); + modelclock_t checkfree = params.checkthreshold; + for(int exec = 0;exec < params.maxexecutions;exec++) { + Thread * t = init_thread; do { + /* Check whether we need to free model actions. */ + + if (params.traceminsize != 0 && + execution->get_curr_seq_num() > checkfree) { + checkfree += params.checkthreshold; + execution->collectActions(); + } + /* * Stash next pending action(s) for thread(s). There * should only need to stash one thread's action--the * 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()) { @@ -455,34 +436,70 @@ void ModelChecker::run() } /* Don't schedule threads which should be disabled */ - for (unsigned int i = 0; i < get_num_threads(); i++) { + 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); } } + for (unsigned int i = 1;i < get_num_threads();i++) { + Thread *th = get_thread(int_to_id(i)); + ModelAction *act = th->get_pending(); + if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ) { + if (act->is_write()) { + std::memory_order order = act->get_mo(); + if (order == std::memory_order_relaxed || \ + order == std::memory_order_release) { + t = th; + break; + } + } else if (act->get_type() == THREAD_CREATE || \ + act->get_type() == PTHREAD_CREATE || \ + act->get_type() == THREAD_START || \ + act->get_type() == THREAD_FINISH) { + t = th; + break; + } + } + } + /* Catch assertions from prior take_step or from - * between-ModelAction bugs (e.g., data races) */ + * between-ModelAction bugs (e.g., data races) */ + if (execution->has_asserted()) break; - if (!t) t = get_next_thread(); if (!t || t->is_model_thread()) break; + if (t->just_woken_up()) { + t->set_wakeup_state(false); + t->set_pending(NULL); + t = NULL; + continue; // Allow this thread to stash the next pending action + } /* Consume the next action for a Thread */ ModelAction *curr = t->get_pending(); t->set_pending(NULL); t = execution->take_step(curr); } while (!should_terminate_execution()); - - } while (next_execution()); - - execution->fixup_release_sequences(); + finish_execution((exec+1) < params.maxexecutions); + //restore random number generator state after rollback + setstate(random_state); + } 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(); + + /* unlink tmp file created by last child process */ + char filename[256]; + snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid()); + unlink(filename); }