From: root Date: Wed, 26 Jun 2019 20:04:49 +0000 (-0700) Subject: Merge branch 'new_fuzzer' of /home/git/random-fuzzer into new_fuzzer X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=bac8bc0661e904fc2b1b9aba07d239679483b2b4;hp=02e8c0e82227e667163f370f663935272599a4ba Merge branch 'new_fuzzer' of /home/git/random-fuzzer into new_fuzzer --- diff --git a/cmodelint.cc b/cmodelint.cc index 348051a0..96cd1c49 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -1,7 +1,9 @@ #include #include "model.h" +#include "execution.h" #include "action.h" #include "cmodelint.h" +#include "snapshot-interface.h" #include "threads-model.h" memory_order orders[6] = { @@ -9,6 +11,18 @@ memory_order orders[6] = { memory_order_release, memory_order_acq_rel, memory_order_seq_cst }; +static void ensureModel(ModelAction * action) { + if (!model) { + if (!model_init) { + snapshot_system_init(10000, 1024, 1024, 40000); + model_init = new ModelChecker(); + } + model_init->get_execution()->check_current_action(action); + } else { + model->switch_to_master(action); + } +} + /** Performs a read action.*/ uint64_t model_read_action(void * obj, memory_order ord) { return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj)); @@ -85,22 +99,22 @@ void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) // cds atomic inits void cds_atomic_init8(void * obj, uint8_t val, const char * position) { - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) ); } void cds_atomic_init16(void * obj, uint16_t val, const char * position) { - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) ); } void cds_atomic_init32(void * obj, uint32_t val, const char * position) { - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) ); } void cds_atomic_init64(void * obj, uint64_t val, const char * position) { - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val) ); } @@ -130,22 +144,22 @@ uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) // cds atomic stores void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) { - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val) ); } void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) { - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val) ); } void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) { - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val) ); } void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) { - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val) ); } diff --git a/execution.cc b/execution.cc index d75499f1..2c08711e 100644 --- a/execution.cc +++ b/execution.cc @@ -778,9 +778,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * /* Last SC fence in the current thread */ ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); - ModelAction *last_sc_write = NULL; - if (curr->is_seqcst()) - last_sc_write = get_last_seq_cst_write(curr); int tid = curr->get_tid(); ModelAction *prev_same_thread = NULL; diff --git a/execution.h b/execution.h index 20bbfdc6..4d5ef866 100644 --- a/execution.h +++ b/execution.h @@ -105,6 +105,7 @@ public: CycleGraph * const get_mo_graph() { return mo_graph; } HashTable * getCondMap() {return &cond_map;} HashTable * getMutexMap() {return &mutex_map;} + ModelAction * check_current_action(ModelAction *curr); SNAPSHOTALLOC private: @@ -124,7 +125,6 @@ private: modelclock_t get_next_seq_num(); bool next_execution(); - ModelAction * check_current_action(ModelAction *curr); bool initialize_curr_action(ModelAction **curr); void process_read(ModelAction *curr, SnapVector * rf_set); void process_write(ModelAction *curr); diff --git a/include/cmodelint.h b/include/cmodelint.h index 8530827c..7bc6a253 100644 --- a/include/cmodelint.h +++ b/include/cmodelint.h @@ -10,8 +10,11 @@ #if __cplusplus using std::memory_order; extern "C" { +#else +typedef int bool; #endif + uint64_t model_read_action(void * obj, memory_order ord); void model_write_action(void * obj, memory_order ord, uint64_t val); void model_init_action(void * obj, uint64_t val); diff --git a/main.cc b/main.cc index 0abc80b7..cc3fcbf0 100644 --- a/main.cc +++ b/main.cc @@ -164,23 +164,6 @@ static void install_trace_analyses(ModelExecution *execution) /** The model_main function contains the main model checking loop. */ static void model_main() { - struct model_params params; - - param_defaults(¶ms); - register_plugins(); - - parse_options(¶ms, main_argc, main_argv); - - //Initialize race detector - initRaceDetector(); - - snapshot_stack_init(); - - if (!model) - model = new ModelChecker(); - model->setParams(params); - install_trace_analyses(model->get_execution()); - snapshot_record(0); model->run(); delete model; @@ -212,6 +195,28 @@ int main(int argc, char **argv) /* Configure output redirection for the model-checker */ redirect_output(); - /* Let's jump in quickly and start running stuff */ - snapshot_system_init(10000, 1024, 1024, 40000, &model_main); + //Initialize snapshotting library + if (!model_init) + snapshot_system_init(10000, 1024, 1024, 40000); + + struct model_params params; + + param_defaults(¶ms); + register_plugins(); + parse_options(¶ms, main_argc, main_argv); + + //Initialize race detector + initRaceDetector(); + + snapshot_stack_init(); + + if (!model_init) + model = new ModelChecker(); + else + model = model_init; + + model->setParams(params); + install_trace_analyses(model->get_execution()); + + startExecution(&model_main); } diff --git a/model.cc b/model.cc index 61d0b64c..c468d0de 100644 --- a/model.cc +++ b/model.cc @@ -18,7 +18,14 @@ #include "execution.h" #include "bugmessage.h" -ModelChecker *model; +ModelChecker *model = NULL; +ModelChecker *model_init = NULL; + +/** Wrapper to run the user's main function, with appropriate arguments */ +void user_main_wrapper(void *) +{ + user_main(model->params.argc, model->params.argv); +} /** @brief Constructor */ ModelChecker::ModelChecker() : @@ -33,6 +40,9 @@ ModelChecker::ModelChecker() : inspect_plugin(NULL) { memset(&stats,0,sizeof(struct execution_stats)); + init_thread = new Thread(execution->get_next_id(), (thrd_t *) malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program + execution->add_thread(init_thread); + scheduler->set_current_thread(init_thread); } /** @brief Destructor */ @@ -310,10 +320,11 @@ 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); - }*/ + + if (inspect_plugin != NULL) { + inspect_plugin->inspectModelAction(act); + } + old->set_pending(act); if (Thread::swap(old, &system_context) < 0) { perror("swap threads"); @@ -322,12 +333,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) return old->get_return_value(); } -/** Wrapper to run the user's main function, with appropriate arguments */ -void user_main_wrapper(void *) -{ - user_main(model->params.argc, model->params.argv); -} - bool ModelChecker::should_terminate_execution() { /* Infeasible -> don't take any more steps */ @@ -363,10 +368,8 @@ void ModelChecker::run() initstate(423121, random_state, sizeof(random_state)); for(int exec = 0;exec < params.maxexecutions;exec++) { - thrd_t user_thread; - 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); - //Need to seed random number generator, otherwise its state gets reset + Thread * t = init_thread; + do { /* * Stash next pending action(s) for thread(s). There diff --git a/model.h b/model.h index 2a505c3d..46c24543 100644 --- a/model.h +++ b/model.h @@ -72,6 +72,7 @@ private: Scheduler * const scheduler; NodeStack * const node_stack; ModelExecution *execution; + Thread * init_thread; int execution_number; @@ -103,5 +104,6 @@ private: }; extern ModelChecker *model; +extern ModelChecker *model_init; #endif /* __MODEL_H__ */ diff --git a/pthread.cc b/pthread.cc index 8c2bc076..79e90425 100644 --- a/pthread.cc +++ b/pthread.cc @@ -48,14 +48,19 @@ void pthread_exit(void *value_ptr) { } int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { - if (!model) { - model = new ModelChecker(); - } - cdsc::mutex *m = new cdsc::mutex(); + ModelExecution *execution; - ModelExecution *execution = model->get_execution(); + if (!model) { + if (!model_init) { + snapshot_system_init(10000, 1024, 1024, 40000); + model_init = new ModelChecker(); + } + execution = model_init->get_execution(); + } else + execution = model->get_execution(); execution->getMutexMap()->put(p_mutex, m); + return 0; } diff --git a/snapshot-interface.h b/snapshot-interface.h index d926c74e..3e3ad71e 100644 --- a/snapshot-interface.h +++ b/snapshot-interface.h @@ -11,8 +11,8 @@ typedef unsigned int snapshot_id; typedef void (*VoidFuncPtr)(); void snapshot_system_init(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, - unsigned int numheappages, VoidFuncPtr entryPoint); - + unsigned int numheappages); +void startExecution(VoidFuncPtr entryPoint); void snapshot_stack_init(); void snapshot_record(int seq_index); int snapshot_backtrack_before(int seq_index); diff --git a/snapshot.cc b/snapshot.cc index ce2b28fe..5c1c1e25 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -134,7 +134,7 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused) static void mprot_snapshot_init(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, - unsigned int numheappages, VoidFuncPtr entryPoint) + unsigned int numheappages) { /* Setup a stack for our signal handler.... */ stack_t ss; @@ -179,7 +179,10 @@ static void mprot_snapshot_init(unsigned int numbackingpages, pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space); model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1); snapshot_add_memory_region(pagealignedbase, numheappages); +} + +static void mprot_startExecution(VoidFuncPtr entryPoint) { entryPoint(); } @@ -363,7 +366,7 @@ mspace create_shared_mspace() static void fork_snapshot_init(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, - unsigned int numheappages, VoidFuncPtr entryPoint) + unsigned int numheappages) { if (!fork_snap) createSharedMemory(); @@ -371,7 +374,9 @@ static void fork_snapshot_init(unsigned int numbackingpages, void *base_model_snapshot_space = malloc((numheappages + 1) * PAGESIZE); void *pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space); model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1); +} +static void fork_startExecution(VoidFuncPtr entryPoint) { /* setup an "exiting" context */ char stack[128]; create_context(&exit_ctxt, stack, sizeof(stack), fork_exit); @@ -437,12 +442,21 @@ static void fork_roll_back(snapshot_id theID) */ void snapshot_system_init(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, - unsigned int numheappages, VoidFuncPtr entryPoint) + unsigned int numheappages) +{ +#if USE_MPROTECT_SNAPSHOT + mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages); +#else + fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages); +#endif +} + +void startExecution(VoidFuncPtr entryPoint) { #if USE_MPROTECT_SNAPSHOT - mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint); + mprot_startExecution(entryPoint); #else - fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint); + fork_startExecution(entryPoint); #endif } diff --git a/test/condvar.cc b/test/condvar.cc index fcfd59a8..0457c414 100644 --- a/test/condvar.cc +++ b/test/condvar.cc @@ -3,11 +3,11 @@ #include "threads.h" #include "librace.h" #include "stdatomic.h" -#include +#include #include -std::mutex * m; -std::condition_variable *v; +cdsc::mutex * m; +cdsc::condition_variable *v; int shareddata; static void a(void *obj) @@ -32,8 +32,8 @@ int user_main(int argc, char **argv) { thrd_t t1, t2; store_32(&shareddata, (unsigned int) 0); - m=new std::mutex(); - v=new std::condition_variable(); + m=new cdsc::mutex(); + v=new cdsc::condition_variable(); thrd_create(&t1, (thrd_start_t)&a, NULL); thrd_create(&t2, (thrd_start_t)&b, NULL);