X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=0f2f0366ebf136f448965c2d5449e317b199ca30;hp=4d62361197dd5c416a15ab6754186e60d679857e;hb=7921811e8bd7bba2cdd892434a58ec7254ae0f99;hpb=df2426d1671efd91afbb8606d877bdf1053cc1ac diff --git a/model.cc b/model.cc index 4d62361..0f2f036 100644 --- a/model.cc +++ b/model.cc @@ -2,6 +2,7 @@ #include #include #include +#include #include "model.h" #include "action.h" @@ -15,6 +16,7 @@ #include "datarace.h" #include "threads-model.h" #include "output.h" +#include "traceanalysis.h" #define INITIAL_THREAD_ID 0 @@ -91,6 +93,7 @@ ModelChecker::ModelChecker(struct model_params params) : thrd_last_action(new SnapVector(1)), thrd_last_fence_release(new SnapVector()), node_stack(new NodeStack()), + trace_analyses(new ModelVector()), priv(new struct model_snapshot_members()), mo_graph(new CycleGraph()) { @@ -120,6 +123,9 @@ ModelChecker::~ModelChecker() delete thrd_last_action; delete thrd_last_fence_release; delete node_stack; + for (unsigned int i = 0; i size();i++) + delete (*trace_analyses)[i]; + delete trace_analyses; delete scheduler; delete mo_graph; delete priv; @@ -154,9 +160,6 @@ void ModelChecker::reset_to_initial_state() DEBUG("+++ Resetting to initial state +++\n"); node_stack->reset_execution(); - /* 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 @@ -286,7 +289,7 @@ Thread * ModelChecker::get_next_thread() } DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid)); ASSERT(tid != THREAD_ID_T_NONE); - return thread_map->get(id_to_int(tid)); + return get_thread(id_to_int(tid)); } /** @@ -422,9 +425,16 @@ bool ModelChecker::is_complete_execution() const * @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) +bool ModelChecker::assert_bug(const char *msg, ...) { - priv->bugs.push_back(new bug_message(msg)); + char str[800]; + + va_list ap; + va_start(ap, msg); + vsnprintf(str, sizeof(str), msg, ap); + va_end(ap); + + priv->bugs.push_back(new bug_message(str)); if (isfeasibleprefix()) { set_assert(); @@ -548,6 +558,7 @@ bool ModelChecker::next_execution() assert_bug("Deadlock detected"); checkDataRaces(); + run_trace_analyses(); } record_stats(); @@ -573,6 +584,15 @@ bool ModelChecker::next_execution() return true; } +/** + * @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(action_trace); + } +} + /** * @brief Find the last fence-related backtracking conflict for a ModelAction * @@ -755,6 +775,7 @@ void ModelChecker::set_backtracking(ModelAction *act) Node *node = prev->get_node()->get_parent(); + /* See Dynamic Partial Order Reduction (addendum), POPL '05 */ int low_tid, high_tid; if (node->enabled_status(t->get_id()) == THREAD_ENABLED) { low_tid = id_to_int(act->get_tid()); @@ -771,6 +792,7 @@ void ModelChecker::set_backtracking(ModelAction *act) if (i >= node->get_num_threads()) break; + /* See Dynamic Partial Order Reduction (addendum), POPL '05 */ /* Don't backtrack into a point where the thread is disabled or sleeping. */ if (node->enabled_status(tid) != THREAD_ENABLED) continue; @@ -1219,9 +1241,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr) } case THREAD_FINISH: { Thread *th = get_thread(curr); - while (!th->wait_list_empty()) { - ModelAction *act = th->pop_wait_list(); - scheduler->wake(get_thread(act)); + /* Wake up any joining threads */ + for (unsigned int i = 0; i < get_num_threads(); i++) { + Thread *waiting = get_thread(int_to_id(i)); + if (waiting->waiting_on() == th && + waiting->get_pending()->is_thread_join()) + scheduler->wake(waiting); } th->complete(); /* Completed thread can't satisfy promises */ @@ -1464,7 +1489,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { } else if (curr->is_thread_join()) { Thread *blocking = curr->get_thread_operand(); if (!blocking->is_complete()) { - blocking->push_wait_list(curr); thread_blocking_check_promises(blocking, get_thread(curr)); return false; } @@ -1488,20 +1512,9 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr) { ASSERT(curr); bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw(); - - if (!check_action_enabled(curr)) { - /* Make the execution look like we chose to run this action - * much later, when a lock/join can succeed */ - get_thread(curr)->set_pending(curr); - scheduler->sleep(get_thread(curr)); - return NULL; - } - bool newly_explored = initialize_curr_action(&curr); DBG(); - if (DBG_ENABLED()) - curr->print(); wake_up_sleeping_actions(curr); @@ -1798,16 +1811,15 @@ bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const } /** - * Updates the mo_graph with the constraints imposed from the current + * @brief Updates the mo_graph with the constraints imposed from the current * read. * * Basic idea is the following: Go through each other thread and find * the last action that happened before our read. Two cases: * - * (1) The action is a write => that write must either occur before + * -# The action is a write: that write must either occur before * the write we read from or be the write we read from. - * - * (2) The action is a read => the write that that action read from + * -# The action is a read: the write that that action read from * must occur before the write we read from or be the same write. * * @param curr The current action. Must be a read. @@ -3076,32 +3088,14 @@ Thread * ModelChecker::take_step(ModelAction *curr) Thread *curr_thrd = get_thread(curr); ASSERT(curr_thrd->get_state() == THREAD_READY); + ASSERT(check_action_enabled(curr)); /* May have side effects? */ curr = check_current_action(curr); - - /* Infeasible -> don't take any more steps */ - if (is_infeasible()) - return NULL; - else if (isfeasibleprefix() && have_bug_reports()) { - set_assert(); - return NULL; - } - - if (params.bound != 0 && priv->used_sequence_numbers > params.bound) - return NULL; + ASSERT(curr); if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd); - Thread *next_thrd = NULL; - if (curr) - next_thrd = action_select_next_thread(curr); - if (!next_thrd) - next_thrd = get_next_thread(); - - DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1, - next_thrd ? id_to_int(next_thrd->get_id()) : -1); - - return next_thrd; + return action_select_next_thread(curr); } /** Wrapper to run the user's main function, with appropriate arguments */ @@ -3110,6 +3104,21 @@ void user_main_wrapper(void *) user_main(model->params.argc, model->params.argv); } +bool ModelChecker::should_terminate_execution() +{ + /* Infeasible -> don't take any more steps */ + if (is_infeasible()) + return true; + else if (isfeasibleprefix() && have_bug_reports()) { + set_assert(); + return true; + } + + if (params.bound != 0 && priv->used_sequence_numbers > params.bound) + return true; + return false; +} + /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { @@ -3131,7 +3140,16 @@ void ModelChecker::run() 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"); + 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 && is_enabled(th) && !check_action_enabled(act)) { + scheduler->sleep(th); } } @@ -3140,11 +3158,16 @@ void ModelChecker::run() if (has_asserted()) break; + if (!t) + t = get_next_thread(); + if (!t || t->is_model_thread()) + 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()); + } while (!should_terminate_execution()); /* * Launch end-of-execution release sequence fixups only when