From: bdemsky Date: Thu, 6 Jun 2019 05:28:53 +0000 (-0700) Subject: refactor choices into own class X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=e16b141f84421c9823e9208240d2ba6eed4d87d9 refactor choices into own class --- diff --git a/Makefile b/Makefile index e47c4ada..5411f583 100644 --- a/Makefile +++ b/Makefile @@ -4,7 +4,7 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \ nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \ datarace.o impatomic.o cmodelint.o \ snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \ - context.o execution.o libannotate.o plugins.o pthread.o futex.o + context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o CPPFLAGS += -Iinclude -I. LDFLAGS := -ldl -lrt -rdynamic diff --git a/classlist.h b/classlist.h index 6d9106fc..09aa09d1 100644 --- a/classlist.h +++ b/classlist.h @@ -1,5 +1,7 @@ #ifndef CLASSLIST_H #define CLASSLIST_H +#include "stl-model.h" + class ClockVector; class CycleGraph; class CycleNode; @@ -11,8 +13,9 @@ class NodeStack; class Scheduler; class Thread; class TraceAnalysis; +class Fuzzer; struct model_snapshot_members; struct bug_message; - +typedef SnapList action_list_t; #endif diff --git a/execution.cc b/execution.cc index dabf5509..a6ed9d68 100644 --- a/execution.cc +++ b/execution.cc @@ -14,6 +14,7 @@ #include "datarace.h" #include "threads-model.h" #include "bugmessage.h" +#include "fuzzer.h" #define INITIAL_THREAD_ID 0 @@ -25,10 +26,7 @@ struct model_snapshot_members { /* First thread created will have id INITIAL_THREAD_ID */ next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), - next_backtrack(NULL), bugs(), - too_many_reads(false), - no_valid_reads(false), bad_synchronization(false), bad_sc_read(false), asserted(false) @@ -42,10 +40,7 @@ struct model_snapshot_members { unsigned int next_thread_id; modelclock_t used_sequence_numbers; - ModelAction *next_backtrack; SnapVector bugs; - bool too_many_reads; - bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; bool bad_sc_read; @@ -73,7 +68,8 @@ ModelExecution::ModelExecution(ModelChecker *m, thrd_last_fence_release(), node_stack(node_stack), priv(new struct model_snapshot_members()), - mo_graph(new CycleGraph()) + mo_graph(new CycleGraph()), + fuzzer(new Fuzzer()) { /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); @@ -289,14 +285,13 @@ bool ModelExecution::is_complete_execution() const */ bool ModelExecution::process_read(ModelAction *curr, ModelVector * rf_set) { - int random_index = random() % rf_set->size(); bool updated = false; - const ModelAction *rf = (*rf_set)[random_index]; + const ModelAction *rf = fuzzer->selectWrite(curr, rf_set); + ASSERT(rf); mo_graph->startChanges(); - updated = r_modification_order(curr, rf); read_from(curr, rf); mo_graph->commitChanges(); @@ -380,20 +375,8 @@ bool ModelExecution::process_mutex(ModelAction *curr) } case ATOMIC_NOTIFY_ONE: { action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); - - //BCD -- TOFIX FUZZER - //THIS SHOULD BE A RANDOM CHOICE - // int wakeupthread = curr->get_node()->get_misc(); - int wakeupthread = 0; - action_list_t::iterator it = waiters->begin(); - - // WL - if (it == waiters->end()) - break; - - advance(it, wakeupthread); - scheduler->wake(get_thread(*it)); - waiters->erase(it); + Thread * thread = fuzzer->selectNotify(waiters); + scheduler->wake(thread); break; } @@ -750,10 +733,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const char *ptr = buf; if (mo_graph->checkForCycles()) ptr += sprintf(ptr, "[mo cycle]"); - if (priv->too_many_reads) - ptr += sprintf(ptr, "[too many reads]"); - if (priv->no_valid_reads) - ptr += sprintf(ptr, "[no valid reads-from]"); if (priv->bad_synchronization) ptr += sprintf(ptr, "[bad sw ordering]"); if (priv->bad_sc_read) @@ -771,8 +750,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const bool ModelExecution::is_infeasible() const { return mo_graph->checkForCycles() || - priv->no_valid_reads || - priv->too_many_reads || priv->bad_synchronization || priv->bad_sc_read; } @@ -1611,3 +1588,6 @@ Thread * ModelExecution::take_step(ModelAction *curr) return action_select_next_thread(curr); } +Fuzzer * ModelExecution::getFuzzer() { + return fuzzer; +} diff --git a/execution.h b/execution.h index d13cc721..737477fe 100644 --- a/execution.h +++ b/execution.h @@ -102,7 +102,7 @@ public: bool is_deadlocked() const; action_list_t * get_action_trace() { return &action_trace; } - + Fuzzer * getFuzzer(); CycleGraph * const get_mo_graph() { return mo_graph; } HashTable * getCondMap() {return &cond_map;} HashTable * getMutexMap() {return &mutex_map;} @@ -206,6 +206,8 @@ private: */ CycleGraph * const mo_graph; + Fuzzer * fuzzer; + Thread * action_select_next_thread(const ModelAction *curr) const; }; diff --git a/fuzzer.cc b/fuzzer.cc new file mode 100644 index 00000000..62097b21 --- /dev/null +++ b/fuzzer.cc @@ -0,0 +1,26 @@ +#include "fuzzer.h" +#include +#include "threads-model.h" +#include "model.h" + +ModelAction * Fuzzer::selectWrite(ModelAction *read, ModelVector * rf_set) { + int random_index = random() % rf_set->size(); + return (*rf_set)[random_index]; +} + +Thread * Fuzzer::selectThread(Node *n, int * threadlist, int numthreads) { + 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); +} + +Thread * Fuzzer::selectNotify(action_list_t * waiters) { + int numwaiters = waiters->size(); + int random_index = random() % numwaiters; + action_list_t::iterator it = waiters->begin(); + advance(it, random_index); + Thread *thread = model->get_thread(*it); + waiters->erase(it); + return thread; +} diff --git a/fuzzer.h b/fuzzer.h new file mode 100644 index 00000000..14d875d7 --- /dev/null +++ b/fuzzer.h @@ -0,0 +1,16 @@ +#ifndef FUZZER_H +#define FUZZER_H +#include "classlist.h" +#include "mymemory.h" +#include "stl-model.h" + +class Fuzzer { +public: + Fuzzer() {} + ModelAction * selectWrite(ModelAction *read, ModelVector* rf_set); + Thread * selectThread(Node *n, int * threadlist, int numthreads); + Thread * selectNotify(action_list_t * waiters); + MEMALLOC +private: +}; +#endif diff --git a/schedule.cc b/schedule.cc index 83616173..fff26ce2 100644 --- a/schedule.cc +++ b/schedule.cc @@ -7,6 +7,7 @@ #include "model.h" #include "nodestack.h" #include "execution.h" +#include "fuzzer.h" /** * Format an "enabled_type_t" for printing @@ -203,29 +204,19 @@ void Scheduler::wake(Thread *t) */ Thread * Scheduler::select_next_thread(Node *n) { - 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; + int avail_threads = 0; + int thread_list[enabled_len]; + for (int i = 0; i< enabled_len; i++) { + if (enabled[i] == THREAD_ENABLED) + thread_list[avail_threads++] = i; } - while (avail_threads > 0) { - int random_index = random() % 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 (enabled[curr_thread_index] == THREAD_ENABLED) { - return model->get_thread(curr_tid); - } else { // remove this threads from available threads - thread_list[random_index] = thread_list[avail_threads - 1]; - avail_threads--; - } - } - - /* No thread was enabled */ - return NULL; + if (avail_threads == 0) + return NULL; // No threads availablex + + Thread * thread = execution->getFuzzer()->selectThread(n, thread_list, avail_threads); + curr_thread_index = id_to_int(thread->get_id()); + return thread; } void Scheduler::set_scheduler_thread(thread_id_t tid) {