From: weiyu Date: Thu, 14 Nov 2019 22:30:19 +0000 (-0800) Subject: Version that finds the bug of iris X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=e296778cb3574eeafdd20e0c25a4081c8d1ab0dc;hp=06bee25f85e35dec1db4247dadde23037b8ec67b Version that finds the bug of iris --- diff --git a/cmodelint.cc b/cmodelint.cc index 3c59fa01..8774c5b3 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -335,6 +335,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) { void cds_func_entry(const char * funcName) { ensureModel(); + /* Thread * th = thread_current(); uint32_t func_id; @@ -355,22 +356,25 @@ void cds_func_entry(const char * funcName) { } history->enter_function(func_id, th->get_id()); +*/ } void cds_func_exit(const char * funcName) { ensureModel(); - Thread * th = thread_current(); + +/* Thread * th = thread_current(); uint32_t func_id; ModelHistory *history = model->get_history(); func_id = history->getFuncMap()->get(funcName); - /* func_id not found; this could happen in the case where a function calls cds_func_entry + * func_id not found; this could happen in the case where a function calls cds_func_entry * when the model has been defined yet, but then an atomic inside the function initializes * the model. And then cds_func_exit is called upon the function exiting. - */ + * if (func_id == 0) return; history->exit_function(func_id, th->get_id()); +*/ } diff --git a/execution.cc b/execution.cc index 5449c480..606b9642 100644 --- a/execution.cc +++ b/execution.cc @@ -282,7 +282,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { add_normal_write_to_lists(act); add_write_to_lists(act); w_modification_order(act); - model->get_history()->process_action(act, act->get_tid()); +// model->get_history()->process_action(act, act->get_tid()); return act; } @@ -302,13 +302,14 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * } // Remove writes that violate read modification order + /* for (uint i = 0; i < rf_set->size(); i++) { ModelAction * rf = (*rf_set)[i]; if (!r_modification_order(curr, rf, NULL, NULL, true)) { (*rf_set)[i] = rf_set->back(); rf_set->pop_back(); } - } + }*/ while(true) { int index = fuzzer->selectWrite(curr, rf_set); @@ -1757,7 +1758,7 @@ Thread * ModelExecution::take_step(ModelAction *curr) ASSERT(curr); /* Process this action in ModelHistory for records */ - model->get_history()->process_action( curr, curr->get_tid() ); +// model->get_history()->process_action( curr, curr->get_tid() ); if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd); diff --git a/newfuzzer.cc b/newfuzzer.cc index 9d061bbf..e76d8961 100644 --- a/newfuzzer.cc +++ b/newfuzzer.cc @@ -33,7 +33,7 @@ void NewFuzzer::register_engine(ModelHistory * history, ModelExecution *executio int NewFuzzer::selectWrite(ModelAction *read, SnapVector * rf_set) { -// return random() % rf_set->size(); + return random() % rf_set->size(); thread_id_t tid = read->get_tid(); int thread_id = id_to_int(tid); @@ -67,35 +67,6 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector * rf_set //model_print("the %d read action of thread %d at %p is unsuccessful\n", read->get_seq_number(), read_thread->get_id(), read->get_location()); -/*-- - Thread * read_thread = execution->get_thread(tid); - bool should_reselect_predicate = true; - bool should_sleep = should_conditional_sleep(selected_branch); - dist_info_vec.clear(); - - if (!find_threads(read)) { - update_predicate_score(selected_branch, SLEEP_FAIL_TYPE1); - should_reselect_predicate = true; - } else if (!should_sleep) { - update_predicate_score(selected_branch, SLEEP_FAIL_TYPE2); - should_reselect_predicate = true; - } else { - for (uint i = 0; i < dist_info_vec.size(); i++) { - struct node_dist_info info = dist_info_vec[i]; - history->add_waiting_thread(tid, info.tid, info.target, info.dist); - } - - // reset thread pending action and revert sequence numbers - read_thread->set_pending(read); - read->reset_seq_number(); - execution->restore_last_seq_num(); - - conditional_sleep(read_thread); - // Returning -1 stops the while loop of ModelExecution::process_read - return -1; - } -*/ - SnapVector * pruned_writes = thrd_pruned_writes[thread_id]; for (uint i = 0; i < pruned_writes->size(); i++) { rf_set->push_back( (*pruned_writes)[i] ); @@ -182,11 +153,6 @@ Predicate * NewFuzzer::selectBranch(thread_id_t tid, Predicate * curr_pred, Func Predicate * child = (*children)[i]; if (child->get_func_inst() == read_inst && !failed_predicates.contains(child)) { branches.push_back(child); - - /*-- max of (exploration counts + 1) - if (child->get_expl_count() + 1 > numerator) - numerator = child->get_expl_count() + 1; - */ } } diff --git a/newfuzzer.h b/newfuzzer.h index ea08b741..63d88de7 100644 --- a/newfuzzer.h +++ b/newfuzzer.h @@ -55,17 +55,17 @@ private: /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite. */ - SnapVector paused_thread_list; - HashTable paused_thread_table; + SnapVector paused_thread_list; //-- (not in use) + HashTable paused_thread_table; //-- HashTable failed_predicates; - SnapVector dist_info_vec; + SnapVector dist_info_vec; //-- - void conditional_sleep(Thread * thread); + void conditional_sleep(Thread * thread); //-- bool should_conditional_sleep(Predicate * predicate); - void wake_up_paused_threads(int * threadlist, int * numthreads); + void wake_up_paused_threads(int * threadlist, int * numthreads); //-- - bool find_threads(ModelAction * pending_read); + bool find_threads(ModelAction * pending_read); //-- /*-- void update_predicate_score(Predicate * predicate, sleep_result_t type); */ bool check_predicate_expressions(PredExprSet * pred_expressions, inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate);