X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=c190e38cacb8c7ccb842957ef07c1c231f3c9bfe;hb=HEAD;hp=4cf5cc57fea4bb94c5998460c701a8b618264c3d;hpb=7d107019dd0d32d0803fb802fc318a57101707a1;p=c11tester.git diff --git a/model.cc b/model.cc index 4cf5cc57..c190e38c 100644 --- a/model.cc +++ b/model.cc @@ -15,12 +15,20 @@ #include "output.h" #include "traceanalysis.h" #include "execution.h" -#include "history.h" #include "bugmessage.h" #include "params.h" #include "plugins.h" ModelChecker *model = NULL; +int inside_model = 0; + +uint64_t get_nanotime() +{ + struct timespec currtime; + clock_gettime(CLOCK_MONOTONIC, &currtime); + + return currtime.tv_nsec; +} void placeholder(void *) { ASSERT(0); @@ -54,7 +62,16 @@ void install_handler() { perror("sigaction(SIGSEGV)"); exit(EXIT_FAILURE); } +} +void createModelIfNotExist() { + if (!model) { + ENTER_MODEL_FLAG; + snapshot_system_init(100000); + model = new ModelChecker(); + model->startChecker(); + EXIT_MODEL_FLAG; + } } /** @brief Constructor */ @@ -62,10 +79,9 @@ ModelChecker::ModelChecker() : /* Initialize default scheduler */ params(), scheduler(new Scheduler()), - history(new ModelHistory()), execution(new ModelExecution(this, scheduler)), execution_number(1), - curr_thread_num(1), + curr_thread_num(MAIN_THREAD_ID), trace_analyses(), inspect_plugin(NULL) { @@ -73,7 +89,8 @@ ModelChecker::ModelChecker() : "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_memory_ops(); + real_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()); @@ -269,7 +286,9 @@ void ModelChecker::print_execution(bool printbugs) const } model_print("\n"); +#ifdef PRINT_TRACE execution->print_summary(); +#endif } /** @@ -302,7 +321,6 @@ void ModelChecker::finish_execution(bool more_executions) clear_program_output(); execution_number ++; - history->set_new_exec_flag(); if (more_executions) reset_to_initial_state(); @@ -342,12 +360,11 @@ void ModelChecker::startRunExecution(Thread *old) { execution->collectActions(); } - thread_chosen = false; - curr_thread_num = 1; + curr_thread_num = MAIN_THREAD_ID; Thread *thr = getNextThread(old); if (thr != nullptr) { scheduler->set_current_thread(thr); - + EXIT_MODEL_FLAG; if (Thread::swap(old, thr) < 0) { perror("swap threads"); exit(EXIT_FAILURE); @@ -379,27 +396,25 @@ Thread* ModelChecker::getNextThread(Thread *old) } ModelAction *act = thr->get_pending(); - if (act && execution->is_enabled(tid)){ + if (act && scheduler->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 (!thread_chosen) { + 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; - thread_chosen = true; } } 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; - thread_chosen = true; } } } @@ -413,7 +428,7 @@ void ModelChecker::finishRunExecution(Thread *old) scheduler->set_current_thread(NULL); /** Reset curr_thread_num to initial value for next execution. */ - curr_thread_num = 1; + curr_thread_num = MAIN_THREAD_ID; /** If we have more executions, we won't make it past this call. */ finish_execution(execution_number < params.maxexecutions); @@ -448,6 +463,8 @@ uint64_t ModelChecker::switch_thread(ModelAction *act) delete act; return 0; } + ENTER_MODEL_FLAG; + DBG(); Thread *old = thread_current(); old->set_state(THREAD_READY); @@ -487,7 +504,7 @@ bool ModelChecker::handleChosenThread(Thread *old) if (!chosen_thread) { chosen_thread = get_next_thread(); } - if (!chosen_thread || chosen_thread->is_model_thread()) { + if (!chosen_thread) { finishRunExecution(old); return false; } @@ -515,12 +532,16 @@ bool ModelChecker::handleChosenThread(Thread *old) void ModelChecker::startChecker() { startExecution(); //Need to initial random number generator state to avoid resets on rollback - initstate(423121, random_state, sizeof(random_state)); + //initstate(423121, random_state, sizeof(random_state)); + uint64_t seed = get_nanotime(); + srandom(seed); snapshot = take_snapshot(); //reset random number generator state - setstate(random_state); + //setstate(random_state); + seed = get_nanotime(); + srandom(seed); install_trace_analyses(get_execution()); redirect_output();