From 76308d1cc00abc4ab775977e9332c4992af2bef5 Mon Sep 17 00:00:00 2001 From: weiyu Date: Thu, 8 Nov 2018 16:08:24 -0800 Subject: [PATCH] improve randomization --- context.h | 3 +- execution.cc | 13 +++++++++ main.cc | 1 - model.cc | 79 +++++++++++++++++++++++++++++++++------------------- nodestack.cc | 8 ++++-- schedule.cc | 24 ++++++++++++---- 6 files changed, 90 insertions(+), 38 deletions(-) diff --git a/context.h b/context.h index ea32d2f5..fb56e247 100644 --- a/context.h +++ b/context.h @@ -7,6 +7,7 @@ #define __CONTEXT_H__ #include +#include #ifdef MAC @@ -15,7 +16,7 @@ int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp); #else /* !MAC */ static inline int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp) -{ +{ return swapcontext(oucp, ucp); } diff --git a/execution.cc b/execution.cc index 861c82a9..0fcf4e8d 100644 --- a/execution.cc +++ b/execution.cc @@ -2877,6 +2877,19 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons /* Do not split atomic RMW */ if (curr->is_rmwr()) return get_thread(curr); + if (curr->is_write()) { +// std::memory_order order = curr->get_mo(); +// switch(order) { +// case std::memory_order_relaxed: +// return get_thread(curr); +// case std::memory_order_release: +// return get_thread(curr); +// defalut: +// return NULL; +// } + return NULL; + } + /* Follow CREATE with the created thread */ if (curr->get_type() == THREAD_CREATE) return curr->get_thread_operand(); diff --git a/main.cc b/main.cc index 61554eaa..0d4a6ad7 100644 --- a/main.cc +++ b/main.cc @@ -100,7 +100,6 @@ static void print_usage(const char *program_name, struct model_params *params) params->verbose, params->uninitvalue, params->maxexecutions); - model_print("Analysis plugins:\n"); exit(EXIT_SUCCESS); } diff --git a/model.cc b/model.cc index 0e65c63c..bfb6d22f 100644 --- a/model.cc +++ b/model.cc @@ -3,6 +3,7 @@ #include #include #include +#include #include "model.h" #include "action.h" @@ -100,10 +101,9 @@ Thread * ModelChecker::get_next_thread() * Have we completed exploring the preselected path? Then let the * scheduler decide */ - if (diverge == NULL) + if (diverge == NULL) // W: diverge is set to NULL permanently return scheduler->select_next_thread(node_stack->get_head()); - /* Else, we are trying to replay an execution */ ModelAction *next = node_stack->get_next()->get_action(); @@ -303,32 +303,40 @@ bool ModelChecker::next_execution() checkDataRaces(); run_trace_analyses(); - } else if (inspect_plugin && !execution->is_complete_execution() && - (execution->too_many_steps())) { - inspect_plugin->analyze(execution->get_action_trace()); - } + } record_stats(); - /* Output */ if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports())) print_execution(complete); else clear_program_output(); - if (complete) - earliest_diverge = NULL; - if (restart_flag) { do_restart(); return true; } +// test code + execution_number++; + reset_to_initial_state(); + node_stack->pop_restofstack(2); +// node_stack->full_reset(); + diverge = NULL; + return false; +/* test + if (complete) + earliest_diverge = NULL; if (exit_flag) return false; - if ((diverge = execution->get_next_backtrack()) == NULL) +// diverge = execution->get_next_backtrack(); + if (diverge == NULL) { + execution_number++; + reset_to_initial_state(); + model_print("Does not diverge\n"); return false; + } if (DBG_ENABLED()) { model_print("Next execution will diverge at:\n"); @@ -342,6 +350,8 @@ bool ModelChecker::next_execution() reset_to_initial_state(); return true; +*/ + } /** @brief Run trace analyses on complete trace */ @@ -400,9 +410,10 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) Thread *old = thread_current(); scheduler->set_current_thread(NULL); ASSERT(!old->get_pending()); +/* W: No plugin if (inspect_plugin != NULL) { - inspect_plugin->inspectModelAction(act); - } + inspect_plugin->inspectModelAction(act); + }*/ old->set_pending(act); if (Thread::swap(old, &system_context) < 0) { perror("swap threads"); @@ -461,11 +472,11 @@ void ModelChecker::do_restart() void ModelChecker::run() { bool has_next; + int i = 0; do { thrd_t user_thread; - Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); + Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program execution->add_thread(t); - do { /* * Stash next pending action(s) for thread(s). There @@ -473,11 +484,12 @@ 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); + switch_from_master(thr); // L: context swapped, and action type of thr changed. if (thr->is_waiting_on(thr)) assert_bug("Deadlock detected (thread %u)", i); } @@ -491,13 +503,30 @@ void ModelChecker::run() scheduler->sleep(th); } } - /* Catch assertions from prior take_step or from * between-ModelAction bugs (e.g., data races) */ + + 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() == THREAD_START || act->get_type() == THREAD_FINISH) { + t = th; + break; + } + } + } + + if (execution->has_asserted()) break; - - if (!t) + if (!t) t = get_next_thread(); if (!t || t->is_model_thread()) break; @@ -509,16 +538,8 @@ void ModelChecker::run() } while (!should_terminate_execution()); has_next = next_execution(); - if (inspect_plugin != NULL && !has_next) { - inspect_plugin->actionAtModelCheckingFinish(); - // Check if the inpect plugin set the restart flag - if (restart_flag) { - model_print("******* Model-checking RESTART: *******\n"); - has_next = true; - do_restart(); - } - } - } while (has_next); + i++; + } while (i<250); // while (has_next); execution->fixup_release_sequences(); diff --git a/nodestack.cc b/nodestack.cc index bacd067d..f1856d36 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -1,5 +1,6 @@ #define __STDC_FORMAT_MACROS #include +#include #include @@ -488,8 +489,11 @@ void Node::add_read_from_past(const ModelAction *act) */ const ModelAction * Node::get_read_from_past() const { - if (read_from_past_idx < read_from_past.size()) - return read_from_past[read_from_past_idx]; + if (read_from_past_idx < read_from_past.size()) { + int random_index = rand() % read_from_past.size(); + return read_from_past[random_index]; + } +// return read_from_past[read_from_past_idx]; else return NULL; } diff --git a/schedule.cc b/schedule.cc index 2ef4c4d2..2a02e307 100644 --- a/schedule.cc +++ b/schedule.cc @@ -214,8 +214,6 @@ void Scheduler::wake(Thread *t) */ Thread * Scheduler::select_next_thread(Node *n) { - int old_curr_thread = curr_thread_index; - bool have_enabled_thread_with_priority = false; if (model->params.fairwindow != 0) { for (int i = 0; i < enabled_len; i++) { @@ -228,8 +226,17 @@ Thread * Scheduler::select_next_thread(Node *n) } } - for (int i = 0; i < enabled_len; i++) { - curr_thread_index = (old_curr_thread + i + 1) % enabled_len; + int avail_threads = enabled_len; // number of available threads + int thread_list[enabled_len]; // keep a list of threads to select from + for (int i = 0; i< enabled_len; i++){ + thread_list[i] = i; + } + + while (avail_threads > 0) { + int random_index = rand() % avail_threads; + curr_thread_index = thread_list[random_index]; // randomly select a thread from available threads + + // curr_thread_index = (curr_thread_index + i + 1) % enabled_len; thread_id_t curr_tid = int_to_id(curr_thread_index); if (model->params.yieldon) { bool bad_thread = false; @@ -240,13 +247,20 @@ Thread * Scheduler::select_next_thread(Node *n) break; } } - if (bad_thread) + if (bad_thread) { + thread_list[random_index] = thread_list[avail_threads - 1]; // remove this threads from available threads + avail_threads--; + continue; + } } if (enabled[curr_thread_index] == THREAD_ENABLED && (!have_enabled_thread_with_priority || n->has_priority(curr_tid))) { return model->get_thread(curr_tid); + } else { // remove this threads from available threads + thread_list[random_index] = thread_list[avail_threads - 1]; + avail_threads--; } } -- 2.34.1