X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=d3692c47c80c5731cc32e9bddc920aa5a7d8bdad;hp=d1e94e5efa4f70c08486abf646b0ef46a3fae324;hb=43124ec9b82ef50d2adb5cdbf0639f5330995a8b;hpb=9151772f7b6bba10099b552d18cde911aeb39c76 diff --git a/model.cc b/model.cc index d1e94e5e..d3692c47 100644 --- a/model.cc +++ b/model.cc @@ -344,6 +344,164 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) return old->get_return_value(); } +void ModelChecker::continueExecution(Thread *old) +{ + if (params.traceminsize != 0 && + execution->get_curr_seq_num() > checkfree) { + checkfree += params.checkthreshold; + execution->collectActions(); + } + thread_chosen = false; + curr_thread_num = 1; + Thread *thr = getNextThread(); + if (thr != nullptr) { + scheduler->set_current_thread(thr); + if (Thread::swap(old, thr) < 0) { + perror("swap threads"); + exit(EXIT_FAILURE); + } + } else + handleChosenThread(old); +} + +Thread* ModelChecker::getNextThread() +{ + Thread *thr = nullptr; + for (unsigned int i = curr_thread_num; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + thr = get_thread(tid); + + if (!thr->is_complete() && !thr->get_pending()) { + curr_thread_num = i; + break; + } + ModelAction *act = thr->get_pending(); + + if (act && execution->is_enabled(thr) && !execution->check_action_enabled(act)) { + scheduler->sleep(thr); + } + + chooseThread(act, thr); + } + return thr; +} + +void ModelChecker::finishExecution(Thread *old) +{ + scheduler->set_current_thread(NULL); + if (Thread::swap(old, &system_context) < 0) { + perror("swap threads"); + exit(EXIT_FAILURE); + } +} + +void ModelChecker::consumeAction() +{ + ModelAction *curr = chosen_thread->get_pending(); + chosen_thread->set_pending(NULL); + chosen_thread = execution->take_step(curr); +} + +void ModelChecker::chooseThread(ModelAction *act, Thread *old) +{ + if (!thread_chosen && act && execution->is_enabled(old) && (old->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) { + chosen_thread = old; + 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 = old; + thread_chosen = true; + } + } +} + +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(); + ASSERT(!old->get_pending()); + + if (inspect_plugin != NULL) { + inspect_plugin->inspectModelAction(act); + } + + old->set_pending(act); + + curr_thread_num++; + Thread* next = getNextThread(); + if (next != nullptr) + handleNewValidThread(old, next); + else + handleChosenThread(old); + + return old->get_return_value(); +} + +void ModelChecker::handleNewValidThread(Thread *old, Thread *next) +{ + if (old->is_waiting_on(old)) + assert_bug("Deadlock detected (thread %u)", curr_thread_num-1); + + ModelAction *act = old->get_pending(); + + if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) { + scheduler->sleep(old); + } + chooseThread(act, old); + + scheduler->set_current_thread(next); + + if (Thread::swap(old, next) < 0) { + perror("swap threads"); + exit(EXIT_FAILURE); + } +} + +void ModelChecker::handleChosenThread(Thread *old) +{ + if (execution->has_asserted()) + finishExecution(old); + if (!chosen_thread) + chosen_thread = get_next_thread(); + if (!chosen_thread || chosen_thread->is_model_thread()) + finishExecution(old); + 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 + if (should_terminate_execution()) + finishExecution(old); + else + continueExecution(old); + } else { + /* Consume the next action for a Thread */ + consumeAction(); + + if (should_terminate_execution()) + finishExecution(old); + else + continueExecution(old); + } +} + static void runChecker() { model->run(); delete model; @@ -372,86 +530,14 @@ void ModelChecker::run() //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; + 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 < 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); - 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; - } - } - } - - /* Catch assertions from prior take_step or from - * 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()); + chosen_thread = init_thread; + thread_chosen = false; + curr_thread_num = 1; + thread_id_t tid = int_to_id(1); + Thread *thr = get_thread(tid); + switch_from_master(thr); finish_execution((exec+1) < params.maxexecutions); //restore random number generator state after rollback setstate(random_state);