X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=8f974762043065de618aea980d89ac2321ec9dcd;hp=84a60a510456fbea7cd6f0e4e6df87499c40ee48;hb=25d73096cfc14c655f94b01bb235cc5efd1d5696;hpb=83d2c33c508986e2435d7a4bf0266c6bf234304e diff --git a/model.cc b/model.cc index 84a60a51..8f974762 100644 --- a/model.cc +++ b/model.cc @@ -7,7 +7,6 @@ #include "model.h" #include "action.h" -#include "nodestack.h" #include "schedule.h" #include "snapshot-interface.h" #include "common.h" @@ -16,36 +15,89 @@ #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() : /* Initialize default scheduler */ params(), - restart_flag(false), scheduler(new Scheduler()), - node_stack(new NodeStack()), - execution(new ModelExecution(this, scheduler, node_stack)), + history(new ModelHistory()), + execution(new ModelExecution(this, scheduler)), execution_number(1), + curr_thread_num(1), 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; delete scheduler; } /** Method to set parameters */ -void ModelChecker::setParams(struct model_params params) { - this->params = params; - execution->setParams(¶ms); +model_params * ModelChecker::getParams() { + return ¶ms; } /** @@ -54,8 +106,6 @@ void ModelChecker::setParams(struct model_params params) { */ 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 @@ -65,7 +115,7 @@ void ModelChecker::reset_to_initial_state() 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 */ @@ -85,6 +135,18 @@ Thread * ModelChecker::get_current_thread() const return scheduler->get_current_thread(); } +/** + * Must be called from user-thread context (e.g., through the global + * thread_current_id() interface) + * + * @return The id of the currently executing Thread. + */ +thread_id_t ModelChecker::get_current_thread_id() const +{ + ASSERT(int_to_id(curr_thread_num) == get_current_thread()->get_id()); + return int_to_id(curr_thread_num); +} + /** * @brief Choose the next thread to execute. * @@ -103,7 +165,7 @@ Thread * ModelChecker::get_next_thread() * Have we completed exploring the preselected path? Then let the * scheduler decide */ - return scheduler->select_next_thread(node_stack->get_head()); + return scheduler->select_next_thread(); } /** @@ -118,7 +180,7 @@ Thread * ModelChecker::get_next_thread() * @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]; @@ -127,7 +189,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); } /** @@ -138,8 +200,8 @@ 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_thread(NULL); } /** @brief Print bug report listing for this execution (if any bugs exist) */ @@ -151,7 +213,7 @@ void ModelChecker::print_bugs() const bugs->size(), bugs->size() > 1 ? "s" : ""); for (unsigned int i = 0;i < bugs->size();i++) - (*bugs)[i]->print(); + (*bugs)[i] -> print(); } /** @@ -162,16 +224,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: @@ -185,9 +244,7 @@ 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); } @@ -222,12 +279,11 @@ 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() || + bool complete = (execution->is_complete_execution() || execution->have_bug_reports()); /* End-of-execution bug checks */ @@ -235,7 +291,6 @@ bool ModelChecker::next_execution() if (execution->is_deadlocked()) assert_bug("Deadlock detected"); - checkDataRaces(); run_trace_analyses(); } @@ -246,21 +301,17 @@ bool ModelChecker::next_execution() else clear_program_output(); - if (restart_flag) { - do_restart(); - return true; - } -// test code - execution_number++; - reset_to_initial_state(); - node_stack->full_reset(); - return false; + execution_number ++; + history->set_new_exec_flag(); + + if (more_executions) + reset_to_initial_state(); } /** @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()); } /** @@ -283,166 +334,203 @@ Thread * ModelChecker::get_thread(const ModelAction *act) const return execution->get_thread(act); } -/** - * 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 - * model-checker context - * - * @param thread The user-thread to switch to - */ -void ModelChecker::switch_from_master(Thread *thread) +void ModelChecker::startRunExecution(Thread *old) { + while (true) { + if (params.traceminsize != 0 && + execution->get_curr_seq_num() > checkfree) { + checkfree += params.checkthreshold; + execution->collectActions(); + } + + curr_thread_num = 1; + Thread *thr = getNextThread(old); + if (thr != nullptr) { + scheduler->set_current_thread(thr); + + if (Thread::swap(old, thr) < 0) { + perror("swap threads"); + exit(EXIT_FAILURE); + } + return; + } + + if (!handleChosenThread(old)) { + return; + } + } +} + +Thread* ModelChecker::getNextThread(Thread *old) { - scheduler->set_current_thread(thread); - Thread::swap(&system_context, thread); + Thread *nextThread = nullptr; + for (unsigned int i = curr_thread_num;i < get_num_threads();i++) { + thread_id_t tid = int_to_id(i); + Thread *thr = get_thread(tid); + + if (!thr->is_complete()) { + if (!thr->get_pending()) { + curr_thread_num = i; + nextThread = thr; + break; + } + } else if (thr != old && !thr->is_freed()) { + thr->freeResources(); + } + + ModelAction *act = thr->get_pending(); + if (act && execution->is_enabled(tid)){ + /* Don't schedule threads which should be disabled */ + if (!execution->check_action_enabled(act)) { + scheduler->sleep(thr); + } + + /* Allow pending relaxed/release stores or thread actions to perform first */ + else if (!chosen_thread) { + if (act->is_write()) { + std::memory_order order = act->get_mo(); + if (order == std::memory_order_relaxed || \ + order == std::memory_order_release) { + chosen_thread = thr; + } + } else if (act->get_type() == THREAD_CREATE || \ + act->get_type() == PTHREAD_CREATE || \ + act->get_type() == THREAD_START || \ + act->get_type() == THREAD_FINISH) { + chosen_thread = thr; + } + } + } + } + return nextThread; } -/** - * 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. May be NULL only if - * trace is exiting via an assertion (see ModelExecution::set_assert and - * ModelExecution::has_asserted). - * @return Return the value returned by the current action - */ -uint64_t ModelChecker::switch_to_master(ModelAction *act) +/* Swap back to system_context and terminate this execution */ +void ModelChecker::finishRunExecution(Thread *old) { + scheduler->set_current_thread(NULL); + + /** Reset curr_thread_num to initial value for next execution. */ + curr_thread_num = 1; + + /** If we have more executions, we won't make it past this call. */ + finish_execution(execution_number < params.maxexecutions); + + + /** We finished the final execution. Print stuff and exit. */ + 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); + + /* Exit. */ + _Exit(0); +} + +uint64_t ModelChecker::switch_thread(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); + old->set_state(THREAD_READY); + ASSERT(!old->get_pending()); -/* W: No plugin - if (inspect_plugin != NULL) { - inspect_plugin->inspectModelAction(act); - }*/ + + if (inspect_plugin != NULL) { + inspect_plugin->inspectModelAction(act); + } + old->set_pending(act); - if (Thread::swap(old, &system_context) < 0) { - perror("swap threads"); - exit(EXIT_FAILURE); + + if (old->is_waiting_on(old)) + assert_bug("Deadlock detected (thread %u)", curr_thread_num); + + Thread* next = getNextThread(old); + if (next != nullptr) { + scheduler->set_current_thread(next); + if (Thread::swap(old, next) < 0) { + perror("swap threads"); + exit(EXIT_FAILURE); + } + } else { + if (handleChosenThread(old)) { + startRunExecution(old); + } } return old->get_return_value(); } -/** Wrapper to run the user's main function, with appropriate arguments */ -void user_main_wrapper(void *) +bool ModelChecker::handleChosenThread(Thread *old) { - user_main(model->params.argc, model->params.argv); -} - -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()) { - execution->set_assert(); + if (execution->has_asserted()) { + finishRunExecution(old); + return false; + } + if (!chosen_thread) { + chosen_thread = get_next_thread(); + } + if (!chosen_thread) { + finishRunExecution(old); + return false; + } + if (chosen_thread->just_woken_up()) { + chosen_thread->set_wakeup_state(false); + chosen_thread->set_pending(NULL); + chosen_thread = NULL; + // Allow this thread to stash the next pending action return true; } - return false; -} -/** @brief Restart ModelChecker upon returning to the run loop of the - * model checker. */ -void ModelChecker::restart() -{ - restart_flag = true; -} + // Consume the next action for a Thread + ModelAction *curr = chosen_thread->get_pending(); + chosen_thread->set_pending(NULL); + chosen_thread = execution->take_step(curr); -void ModelChecker::do_restart() -{ - restart_flag = false; - reset_to_initial_state(); - node_stack->full_reset(); - memset(&stats,0,sizeof(struct execution_stats)); - execution_number = 1; + if (should_terminate_execution()) { + finishRunExecution(old); + return false; + } else { + return true; + } } -/** @brief Run ModelChecker for the user program */ -void ModelChecker::run() -{ +void ModelChecker::startChecker() { + startExecution(); //Need to initial random number generator state to avoid resets on rollback - char random_state[256]; initstate(423121, random_state, sizeof(random_state)); - for(int exec = 0;exec < params.maxexecutions;exec++) { - thrd_t user_thread; - Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program - execution->add_thread(t); - //Need to seed random number generator, otherwise its state gets reset - do { - /* - * 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 < 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()) { - switch_from_master(thr); // L: context swapped, and action type of thr changed. - if (thr->is_waiting_on(thr)) - assert_bug("Deadlock detected (thread %u)", i); - } - } - - /* Don't schedule threads which should be disabled */ - 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 && 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; - } - } - } + snapshot = take_snapshot(); - /* Catch assertions from prior take_step or from - * between-ModelAction bugs (e.g., data races) */ + //reset random number generator state + setstate(random_state); - if (execution->has_asserted()) - break; - if (!t) - t = get_next_thread(); - if (!t || t->is_model_thread()) - break; + install_trace_analyses(get_execution()); + redirect_output(); + initMainThread(); +} - /* 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()); - next_execution(); - //restore random number generator state after rollback - setstate(random_state); +bool ModelChecker::should_terminate_execution() +{ + if (execution->have_bug_reports()) { + execution->set_assert(); + return true; + } else if (execution->isFinished()) { + return true; } - - 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(); + return false; }