X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=newfuzzer.h;h=db25cfd8744a8801ba4015de686c7c8199025cf4;hb=142611a435d4dca04179bb04be47a3f6dc291b28;hp=f50c47651fa01ded23ec65db13d951edf2e543c0;hpb=c522e1dd1ccc11827ac2fce444764081dca25746;p=c11tester.git diff --git a/newfuzzer.h b/newfuzzer.h index f50c4765..db25cfd8 100644 --- a/newfuzzer.h +++ b/newfuzzer.h @@ -6,21 +6,42 @@ #include "mymemory.h" #include "stl-model.h" +typedef HashTable inst_act_map_t; + class NewFuzzer : public Fuzzer { public: - NewFuzzer() {} + NewFuzzer(); int selectWrite(ModelAction *read, SnapVector* rf_set); + Predicate * get_selected_child_branch(thread_id_t tid); + 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); - bool shouldSleep(const ModelAction *sleep); - bool shouldWake(const ModelAction *sleep); + bool shouldSleep(const ModelAction * sleep); + bool shouldWake(const ModelAction * sleep); + bool shouldWait(const ModelAction * wait); void register_engine(ModelHistory * history, ModelExecution * execution); - MEMALLOC + SNAPSHOTALLOC private: ModelHistory * history; ModelExecution * execution; + + SnapVector thrd_last_read_act; + 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__ */