From: bdemsky Date: Wed, 26 Jun 2019 17:20:49 +0000 (-0700) Subject: redo model object initialization X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=febd10a6b4b1af40b690219ebfd8d0b1a42b183c redo model object initialization --- diff --git a/cmodelint.cc b/cmodelint.cc index 348051a0..c55b9386 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -2,6 +2,7 @@ #include "model.h" #include "action.h" #include "cmodelint.h" +#include "snapshot-interface.h" #include "threads-model.h" memory_order orders[6] = { @@ -9,6 +10,13 @@ memory_order orders[6] = { memory_order_release, memory_order_acq_rel, memory_order_seq_cst }; +static void ensureModel() { + if (!model) { + snapshot_system_init(10000, 1024, 1024, 40000); + model = new ModelChecker(); + } +} + /** 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,21 +93,25 @@ 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) { + ensureModel(); model->switch_to_master( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) ); } void cds_atomic_init16(void * obj, uint16_t val, const char * position) { + ensureModel(); model->switch_to_master( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) ); } void cds_atomic_init32(void * obj, uint32_t val, const char * position) { + ensureModel(); model->switch_to_master( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) ); } void cds_atomic_init64(void * obj, uint64_t val, const char * position) { + ensureModel(); model->switch_to_master( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val) ); @@ -130,21 +142,25 @@ 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) { + ensureModel(); model->switch_to_master( 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) { + ensureModel(); model->switch_to_master( 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) { + ensureModel(); model->switch_to_master( 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) { + ensureModel(); model->switch_to_master( new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val) ); 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..56ad5805 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,25 @@ 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) + 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) + model = new ModelChecker(); + model->setParams(params); + install_trace_analyses(model->get_execution()); + + startExecution(&model_main); } diff --git a/pthread.cc b/pthread.cc index 8c2bc076..35af63e6 100644 --- a/pthread.cc +++ b/pthread.cc @@ -49,6 +49,7 @@ void pthread_exit(void *value_ptr) { int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { if (!model) { + snapshot_system_init(10000, 1024, 1024, 40000); model = new ModelChecker(); } 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 }