X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=a934d0adcb7be451907d3141243f4239564743d2;hb=5d3037f7280786b48caa804d92aa360a6dea846d;hp=c468d0deb3e8b6972673d3910670e99eff42052f;hpb=bac8bc0661e904fc2b1b9aba07d239679483b2b4;p=c11tester.git diff --git a/model.cc b/model.cc index c468d0de..a934d0ad 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,15 +15,15 @@ #include "output.h" #include "traceanalysis.h" #include "execution.h" +#include "history.h" #include "bugmessage.h" +#include "params.h" +#include "plugins.h" ModelChecker *model = NULL; -ModelChecker *model_init = NULL; -/** Wrapper to run the user's main function, with appropriate arguments */ -void user_main_wrapper(void *) -{ - user_main(model->params.argc, model->params.argv); +void placeholder(void *) { + ASSERT(0); } /** @brief Constructor */ @@ -33,29 +32,42 @@ ModelChecker::ModelChecker() : 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), 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 *) malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program + 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 */ + redirect_output(); + install_trace_analyses(get_execution()); } /** @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; } /** @@ -73,7 +85,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 */ @@ -111,7 +123,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(); } /** @@ -126,7 +138,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]; @@ -135,7 +147,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); } /** @@ -146,8 +158,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_to_master(NULL); } /** @brief Print bug report listing for this execution (if any bugs exist) */ @@ -159,7 +171,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(); } /** @@ -170,16 +182,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: @@ -193,9 +202,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); } @@ -234,8 +241,7 @@ bool ModelChecker::next_execution() { 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 */ @@ -243,7 +249,6 @@ bool ModelChecker::next_execution() if (execution->is_deadlocked()) assert_bug("Deadlock detected"); - checkDataRaces(); run_trace_analyses(); } @@ -259,15 +264,16 @@ bool ModelChecker::next_execution() return true; } // test code - execution_number++; + execution_number ++; reset_to_initial_state(); + history->set_new_exec_flag(); return false; } /** @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()); } /** @@ -316,6 +322,16 @@ 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); @@ -333,14 +349,24 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) return old->get_return_value(); } +static void runChecker() { + model->run(); + delete model; +} + +void ModelChecker::startChecker() { + startExecution(get_system_context(), runChecker); + snapshot = take_snapshot(); + 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; + } else if (execution->isFinished()) { + return true; } return false; } @@ -377,12 +403,11 @@ void ModelChecker::run() * 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. + switch_from_master(thr); if (thr->is_waiting_on(thr)) assert_bug("Deadlock detected (thread %u)", i); } @@ -427,6 +452,12 @@ void ModelChecker::run() 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(); @@ -444,4 +475,9 @@ void ModelChecker::run() /* 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); }