X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=b09a81085062533ccc3a5cfa68e808ef82b2e45f;hb=0c429b461653b8e02e515819d89b7acd241996ca;hp=f5dd7cbda419209acf023c27d340218d146ebcff;hpb=18c6031154215ab85ad74fe70deb50ac8e3cbdf6;p=model-checker.git diff --git a/model.cc b/model.cc index f5dd7cb..b09a810 100644 --- a/model.cc +++ b/model.cc @@ -39,7 +39,6 @@ struct bug_message { */ struct model_snapshot_members { model_snapshot_members() : - current_action(NULL), /* First thread created will have id INITIAL_THREAD_ID */ next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), @@ -59,7 +58,6 @@ struct model_snapshot_members { bugs.clear(); } - ModelAction *current_action; unsigned int next_thread_id; modelclock_t used_sequence_numbers; ModelAction *next_backtrack; @@ -161,6 +159,14 @@ void ModelChecker::reset_to_initial_state() /* Print all model-checker output before rollback */ fflush(model_out); + /** + * 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++) + delete get_thread(int_to_id(i))->get_pending(); + snapshot_backtrack_before(0); } @@ -218,7 +224,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) if (curr != NULL) { /* Do not split atomic actions. */ if (curr->is_rmwr()) - return thread_current(); + return get_thread(curr); else if (curr->get_type() == THREAD_CREATE) return curr->get_thread_operand(); } @@ -295,11 +301,8 @@ 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() == NULL) { - scheduler->next_thread(thr); - Thread::swap(&system_context, thr); - priv->current_action->set_sleep_flag(); - thr->set_pending(priv->current_action); + if (scheduler->is_sleep_set(thr) && thr->get_pending()) { + thr->get_pending()->set_sleep_flag(); } } } @@ -324,11 +327,22 @@ void ModelChecker::set_bad_synchronization() priv->bad_synchronization = true; } +/** + * Check whether the current trace has triggered an assertion which should halt + * its execution. + * + * @return True, if the execution should be aborted; false otherwise + */ bool ModelChecker::has_asserted() const { return priv->asserted; } +/** + * Trigger a trace assertion which should cause this execution to be halted. + * This can be due to a detected bug or due to an infeasibility that should + * halt ASAP. + */ void ModelChecker::set_assert() { priv->asserted = true; @@ -1215,16 +1229,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { return true; } -/** - * Stores the ModelAction for the current thread action. Call this - * immediately before switching from user- to system-context to pass - * data between them. - * @param act The ModelAction created by the user-thread action - */ -void ModelChecker::set_current_action(ModelAction *act) { - priv->current_action = act; -} - /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -2663,6 +2667,19 @@ 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 + * model-checker context + * + * @param thread The user-thread to switch to + */ +void ModelChecker::switch_from_master(Thread *thread) +{ + scheduler->next_thread(thread); + Thread::swap(&system_context, thread); +} + /** * 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 @@ -2678,7 +2695,8 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) { DBG(); Thread *old = thread_current(); - set_current_action(act); + ASSERT(!old->get_pending()); + old->set_pending(act); if (Thread::swap(old, &system_context) < 0) { perror("swap threads"); exit(EXIT_FAILURE); @@ -2694,9 +2712,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) */ Thread * ModelChecker::take_step(ModelAction *curr) { - if (has_asserted()) - return NULL; - Thread *curr_thrd = get_thread(curr); ASSERT(curr_thrd->get_state() == THREAD_READY); @@ -2717,42 +2732,14 @@ Thread * ModelChecker::take_step(ModelAction *curr) scheduler->remove_thread(curr_thrd); Thread *next_thrd = get_next_thread(curr); - next_thrd = scheduler->next_thread(next_thrd); + /* Only ask for the next thread from Scheduler if we haven't chosen one + * already */ + if (!next_thrd) + next_thrd = scheduler->next_thread(next_thrd); DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1, next_thrd ? id_to_int(next_thrd->get_id()) : -1); - /* - * Launch end-of-execution release sequence fixups only when there are: - * - * (1) no more user threads to run (or when execution replay chooses - * the 'model_thread') - * (2) pending release sequences - * (3) pending assertions (i.e., data races) - * (4) no pending promises - */ - if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) && - is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) { - model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n", - pending_rel_seqs->size()); - ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, - std::memory_order_seq_cst, NULL, VALUE_NONE, - model_thread); - set_current_action(fixup); - return model_thread; - } - - /* next_thrd == NULL -> don't take any more steps */ - if (!next_thrd) - return NULL; - - if (next_thrd->get_pending() != NULL) { - /* restart a pending action */ - set_current_action(next_thrd->get_pending()); - next_thrd->set_pending(NULL); - return next_thrd; - } - return next_thrd; } @@ -2771,11 +2758,51 @@ void ModelChecker::run() add_thread(t); do { - scheduler->next_thread(t); - Thread::swap(&system_context, t); - t = take_step(priv->current_action); + /* + * 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); + } + } + + /* Catch assertions from prior take_step or from + * between-ModelAction bugs (e.g., data races) */ + if (has_asserted()) + break; + + /* Consume the next action for a Thread */ + ModelAction *curr = t->get_pending(); + t->set_pending(NULL); + t = take_step(curr); } while (t && !t->is_model_thread()); - /** @TODO Re-write release sequence fixups here */ + + /* + * Launch end-of-execution release sequence fixups only when + * the execution is otherwise feasible AND there are: + * + * (1) pending release sequences + * (2) pending assertions that could be invalidated by a change + * in clock vectors (i.e., data races) + * (3) no pending promises + */ + while (!pending_rel_seqs->empty() && + is_feasible_prefix_ignore_relseq() && + !unrealizedraces.empty()) { + model_print("*** WARNING: release sequence fixup action " + "(%zu pending release seuqence(s)) ***\n", + pending_rel_seqs->size()); + ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, + std::memory_order_seq_cst, NULL, VALUE_NONE, + model_thread); + take_step(fixup); + }; } while (next_execution()); print_stats();