From: weiyu Date: Thu, 5 Sep 2019 00:49:56 +0000 (-0700) Subject: When an atomic read action cannot read from a desired write, make this thread sleep... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=eed2c95c816686f295d6baa6743f74d9265b40c2;p=c11tester.git When an atomic read action cannot read from a desired write, make this thread sleep; half working now, still got some bug to fix --- diff --git a/action.cc b/action.cc index 473d99f7..f6d536ee 100644 --- a/action.cc +++ b/action.cc @@ -219,6 +219,11 @@ void ModelAction::set_seq_number(modelclock_t num) seq_number = num; } +void ModelAction::reset_seq_number() +{ + seq_number = 0; +} + bool ModelAction::is_thread_start() const { return type == THREAD_START; diff --git a/action.h b/action.h index 00289355..21d46e5b 100644 --- a/action.h +++ b/action.h @@ -122,6 +122,7 @@ public: void copy_from_new(ModelAction *newaction); void set_seq_number(modelclock_t num); + void reset_seq_number(); void set_try_lock(bool obtainedlock); bool is_thread_start() const; bool is_thread_join() const; diff --git a/execution.cc b/execution.cc index c3cb3bbd..fe27e2ff 100644 --- a/execution.cc +++ b/execution.cc @@ -130,6 +130,12 @@ modelclock_t ModelExecution::get_next_seq_num() return ++priv->used_sequence_numbers; } +/** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */ +void ModelExecution::restore_last_seq_num() +{ + priv->used_sequence_numbers--; +} + /** * @brief Should the current action wake up a given thread? * @@ -282,7 +288,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { * @param rf_set is the set of model actions we can possibly read from * @return True if processing this read updates the mo_graph. */ -void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) +bool ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { SnapVector * priorset = new SnapVector(); bool hasnonatomicstore = hasNonAtomicStore(curr->get_location()); @@ -294,7 +300,7 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector * while(true) { int index = fuzzer->selectWrite(curr, rf_set); if (index == -1) // no feasible write exists - return; + return false; ModelAction *rf = (*rf_set)[index]; @@ -311,7 +317,7 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector * int tid = id_to_int(curr->get_tid()); (*obj_thrd_map.get(curr->get_location()))[tid].pop_back(); } - return; + return true; } priorset->clear(); (*rf_set)[index] = rf_set->back(); @@ -689,11 +695,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) rf_set = build_may_read_from(curr); if (curr->is_read() && !second_part_of_rmw) { - process_read(curr, rf_set); + bool success = process_read(curr, rf_set); delete rf_set; - } else { + if (!success) + return curr; // Do not add action to lists + } else ASSERT(rf_set == NULL); - } /* Add the action to lists */ if (!second_part_of_rmw && curr->get_type() != NOOP) diff --git a/execution.h b/execution.h index f97832d8..da3544ab 100644 --- a/execution.h +++ b/execution.h @@ -93,6 +93,8 @@ public: bool isFinished() {return isfinished;} void setFinished() {isfinished = true;} + void restore_last_seq_num(); + SNAPSHOTALLOC private: int get_execution_number() const; @@ -112,7 +114,7 @@ private: bool next_execution(); bool initialize_curr_action(ModelAction **curr); - void process_read(ModelAction *curr, SnapVector * rf_set); + bool process_read(ModelAction *curr, SnapVector * rf_set); void process_write(ModelAction *curr); bool process_fence(ModelAction *curr); bool process_mutex(ModelAction *curr); diff --git a/fuzzer.h b/fuzzer.h index 348225c8..29d31eda 100644 --- a/fuzzer.h +++ b/fuzzer.h @@ -10,7 +10,8 @@ public: Fuzzer() {} virtual int selectWrite(ModelAction *read, SnapVector* rf_set); virtual Predicate * get_selected_child_branch(thread_id_t tid) = 0; - Thread * selectThread(int * threadlist, int numthreads); + virtual bool has_paused_threads() { return false; } + virtual Thread * selectThread(int * threadlist, int numthreads); Thread * selectNotify(action_list_t * waiters); bool shouldSleep(const ModelAction *sleep); bool shouldWake(const ModelAction *sleep); diff --git a/newfuzzer.cc b/newfuzzer.cc index e09175ce..68efd37d 100644 --- a/newfuzzer.cc +++ b/newfuzzer.cc @@ -4,12 +4,14 @@ #include "action.h" #include "execution.h" #include "funcnode.h" +#include "schedule.h" NewFuzzer::NewFuzzer() : thrd_last_read_act(), thrd_curr_pred(), thrd_selected_child_branch(), - thrd_pruned_writes() + thrd_pruned_writes(), + paused_thread_set() {} /** @@ -47,9 +49,21 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector * rf_set // TODO: make this thread sleep if no write satisfies the chosen predicate // if no read satisfies the selected predicate if ( rf_set->size() == 0 ) { + Thread * read_thread = execution->get_thread(tid); + model_print("the %d read action of thread %d is unsuccessful\n", read->get_seq_number(), read_thread->get_id()); + + read_thread->set_pending(read); + read->reset_seq_number(); // revert some operations + execution->restore_last_seq_num(); + + conditional_sleep(read_thread); + 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] ); + pruned_writes->clear(); +*/ } ASSERT(rf_set->size() != 0); @@ -186,3 +200,46 @@ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred, return pruned; } + +/* @brief Put a thread to sleep because no writes in rf_set satisfies the selected predicate. + * + * @param thread A thread whose last action is a read + */ +void NewFuzzer::conditional_sleep(Thread * thread) +{ + model->getScheduler()->add_sleep(thread); + paused_thread_set.push_back(thread); +} + +bool NewFuzzer::has_paused_threads() +{ + return paused_thread_set.size() != 0; +} + +Thread * NewFuzzer::selectThread(int * threadlist, int numthreads) +{ + if (numthreads == 0 && has_paused_threads()) { + wake_up_paused_threads(threadlist, &numthreads); + model_print("list size: %d\n", numthreads); + model_print("active t id: %d\n", threadlist[0]); + } + + int random_index = random() % numthreads; + int thread = threadlist[random_index]; + thread_id_t curr_tid = int_to_id(thread); + return model->get_thread(curr_tid); +} + +void NewFuzzer::wake_up_paused_threads(int * threadlist, int * numthreads) +{ + int random_index = random() % paused_thread_set.size(); + Thread * thread = paused_thread_set[random_index]; + model->getScheduler()->remove_sleep(thread); + + paused_thread_set[random_index] = paused_thread_set.back(); + paused_thread_set.pop_back(); + + model_print("thread %d is woken up\n", thread->get_id()); + threadlist[*numthreads] = thread->get_id(); + (*numthreads)++; +} diff --git a/newfuzzer.h b/newfuzzer.h index c956935e..7de4cd76 100644 --- a/newfuzzer.h +++ b/newfuzzer.h @@ -12,9 +12,10 @@ class NewFuzzer : public Fuzzer { public: NewFuzzer(); int selectWrite(ModelAction *read, SnapVector* rf_set); - Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst); Predicate * get_selected_child_branch(thread_id_t tid); - bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector * rf_set, inst_act_map_t * inst_act_map); + void conditional_sleep(Thread * thread); + bool has_paused_threads(); + void wake_up_paused_threads(int * threadlist, int * numthreads); Thread * selectThread(int * threadlist, int numthreads); Thread * selectNotify(action_list_t * waiters); @@ -32,6 +33,14 @@ private: SnapVector thrd_curr_pred; SnapVector thrd_selected_child_branch; SnapVector< SnapVector *> thrd_pruned_writes; + + bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector * rf_set, inst_act_map_t * inst_act_map); + Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst); + + /* Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. + * Only used by selectWrite; + */ + SnapVector paused_thread_set; }; #endif /* end of __NEWFUZZER_H__ */ diff --git a/schedule.cc b/schedule.cc index cb97d5bd..4a9752a7 100644 --- a/schedule.cc +++ b/schedule.cc @@ -208,8 +208,8 @@ Thread * Scheduler::select_next_thread() thread_list[avail_threads++] = i; } - if (avail_threads == 0) - return NULL;// No threads availablex + if (avail_threads == 0 && !execution->getFuzzer()->has_paused_threads()) + return NULL; // No threads available Thread * thread = execution->getFuzzer()->selectThread(thread_list, avail_threads); curr_thread_index = id_to_int(thread->get_id());