From 803cd3e461cf355c118a8b1e6cd54bac6b14284c Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 26 Jun 2019 13:02:28 -0700 Subject: [PATCH] More changes --- cmodelint.cc | 36 +++++++++++++++++------------------- execution.h | 2 +- main.cc | 7 +++++-- model.cc | 33 ++++++++++++++++++--------------- model.h | 2 ++ pthread.cc | 16 ++++++++++------ 6 files changed, 53 insertions(+), 43 deletions(-) diff --git a/cmodelint.cc b/cmodelint.cc index c55b9386..96cd1c49 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -1,5 +1,6 @@ #include #include "model.h" +#include "execution.h" #include "action.h" #include "cmodelint.h" #include "snapshot-interface.h" @@ -10,10 +11,15 @@ memory_order orders[6] = { memory_order_release, memory_order_acq_rel, memory_order_seq_cst }; -static void ensureModel() { +static void ensureModel(ModelAction * action) { if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); + 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); } } @@ -93,26 +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) { - ensureModel(); - 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) { - ensureModel(); - 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) { - ensureModel(); - 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) { - ensureModel(); - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val) ); } @@ -142,26 +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) { - ensureModel(); - 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) { - ensureModel(); - 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) { - ensureModel(); - 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) { - ensureModel(); - model->switch_to_master( + ensureModel( new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val) ); } 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/main.cc b/main.cc index 56ad5805..cc3fcbf0 100644 --- a/main.cc +++ b/main.cc @@ -196,7 +196,7 @@ int main(int argc, char **argv) redirect_output(); //Initialize snapshotting library - if (!model) + if (!model_init) snapshot_system_init(10000, 1024, 1024, 40000); struct model_params params; @@ -210,8 +210,11 @@ int main(int argc, char **argv) snapshot_stack_init(); - if (!model) + if (!model_init) model = new ModelChecker(); + else + model = model_init; + model->setParams(params); install_trace_analyses(model->get_execution()); diff --git a/model.cc b/model.cc index 84a60a51..4b159aa5 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 */ @@ -313,10 +323,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"); @@ -325,12 +336,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 */ @@ -367,10 +372,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 35af63e6..79e90425 100644 --- a/pthread.cc +++ b/pthread.cc @@ -48,15 +48,19 @@ 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(); - } - 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; } -- 2.34.1