From: bdemsky Date: Thu, 27 Jun 2019 21:39:01 +0000 (-0700) Subject: revamp scheduler so we can start threads early X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c56ca6ef155dc69125bfc53bf9893016b699a0c2;p=c11tester.git revamp scheduler so we can start threads early --- diff --git a/cmodelint.cc b/cmodelint.cc index 9ea1b681..b1a8eb43 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -14,29 +14,13 @@ memory_order orders[6] = { memory_order_release, memory_order_acq_rel, memory_order_seq_cst }; -#define ensureModel(action) \ - if (!modelchecker_started) { \ - if (!model) { \ - snapshot_system_init(10000, 1024, 1024, 40000); \ - model = new ModelChecker(); \ - } \ - model->get_execution()->check_current_action(action); \ - }else { \ - model->switch_to_master(action); \ - } - - -#define ensureModelValue(action, type) \ - if (!modelchecker_started) { \ - if (!model) { \ - snapshot_system_init(10000, 1024, 1024, 40000); \ - model = new ModelChecker(); \ - } \ - model->get_execution()->check_current_action(action); \ - return (type) thread_current()->get_return_value(); \ - } else { \ - return (type) model->switch_to_master(action); \ +static void ensureModel() { + if (!model) { + snapshot_system_init(10000, 1024, 1024, 40000); + model = new ModelChecker(); + model->startChecker(); } +} /** Performs a read action.*/ uint64_t model_read_action(void * obj, memory_order ord) { @@ -89,85 +73,83 @@ void model_fence_action(memory_order ord) { /* --- helper functions --- */ uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) { - ensureModelValue( - new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size), uint64_t - ); + ensureModel(); + return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size)); } uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) { - ensureModelValue(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj), uint64_t); + ensureModel(); + return model->switch_to_master(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)); } void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) { - ensureModel(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)); + ensureModel(); + model->switch_to_master(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)); } void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) { - ensureModel(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)); + ensureModel(); + model->switch_to_master(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)); } // cds atomic inits void cds_atomic_init8(void * obj, uint8_t val, const char * position) { - ensureModel( - new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) - ); + 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( - new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) - ); + 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( - new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val) - ); + 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( - new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val) - ); + ensureModel(); + model->switch_to_master(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)); } // cds atomic loads uint8_t cds_atomic_load8(void * obj, int atomic_index, const char * position) { - ensureModelValue( - new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint8_t); + ensureModel(); + return (uint8_t) model->switch_to_master( + new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)); } uint16_t cds_atomic_load16(void * obj, int atomic_index, const char * position) { - ensureModelValue( - new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint16_t); + ensureModel(); + return (uint16_t) model->switch_to_master( + new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)); } uint32_t cds_atomic_load32(void * obj, int atomic_index, const char * position) { - ensureModelValue( - new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint32_t + ensureModel(); + return (uint32_t) model->switch_to_master( + new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj) ); } uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) { - ensureModelValue( - new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint64_t); + ensureModel(); + return model->switch_to_master( + new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)); } // cds atomic stores void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) { - ensureModel( - new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val) - ); + 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( - new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val) - ); + 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( - new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val) - ); + 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( - new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val) - ); + ensureModel(); + model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)); } #define _ATOMIC_RMW_(__op__, size, addr, val, atomic_index, position) \ diff --git a/execution.cc b/execution.cc index 2e744251..2c08711e 100644 --- a/execution.cc +++ b/execution.cc @@ -64,7 +64,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack 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 */ diff --git a/main.cc b/main.cc index df6fff68..a484f497 100644 --- a/main.cc +++ b/main.cc @@ -161,16 +161,6 @@ static void install_trace_analyses(ModelExecution *execution) } } -/** The model_main function contains the main model checking loop. */ -static void model_main() -{ - snapshot_record(0); - model->run(); - delete model; - - DEBUG("Exiting\n"); -} - /** * Main function. Just initializes snapshotting library and the * snapshotting library calls the model_main function. @@ -199,6 +189,7 @@ int main(int argc, char **argv) if (!model) { snapshot_system_init(10000, 1024, 1024, 40000); model = new ModelChecker(); + model->startChecker(); } register_plugins(); @@ -213,7 +204,7 @@ int main(int argc, char **argv) snapshot_stack_init(); install_trace_analyses(model->get_execution()); - //Start everything up - modelchecker_started = true; - startExecution(&model_main); + snapshot_record(0); + model->startMainThread(); + DEBUG("Exiting\n"); } diff --git a/model.cc b/model.cc index 0a7913bf..7f38adc3 100644 --- a/model.cc +++ b/model.cc @@ -21,7 +21,6 @@ #include "params.h" ModelChecker *model = NULL; -bool modelchecker_started = false; /** Wrapper to run the user's main function, with appropriate arguments */ void user_main_wrapper(void *) @@ -163,7 +162,7 @@ void ModelChecker::print_bugs() const bugs->size(), bugs->size() > 1 ? "s" : ""); for (unsigned int i = 0;i < bugs->size();i++) - (*bugs)[i] -> print(); + (*bugs)[i]->print(); } /** @@ -174,15 +173,15 @@ void ModelChecker::print_bugs() const */ void ModelChecker::record_stats() { - stats.num_total ++; + stats.num_total++; if (!execution->isfeasibleprefix()) - stats.num_infeasible ++; + stats.num_infeasible++; else if (execution->have_bug_reports()) - stats.num_buggy_executions ++; + stats.num_buggy_executions++; else if (execution->is_complete_execution()) - stats.num_complete ++; + stats.num_complete++; else { - stats.num_redundant ++; + stats.num_redundant++; /** * @todo We can violate this ASSERT() when fairness/sleep sets @@ -263,15 +262,15 @@ bool ModelChecker::next_execution() return true; } // test code - execution_number ++; + execution_number++; reset_to_initial_state(); return false; } /** @brief Run trace analyses on complete trace */ void ModelChecker::run_trace_analyses() { - for (unsigned int i = 0;i < trace_analyses.size();i ++) - trace_analyses[i] -> analyze(execution->get_action_trace()); + for (unsigned int i = 0;i < trace_analyses.size();i++) + trace_analyses[i]->analyze(execution->get_action_trace()); } /** @@ -337,6 +336,15 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) return old->get_return_value(); } +static void runChecker() { + model->run(); + delete model; +} + +void ModelChecker::startChecker() { + startExecution(get_system_context(), runChecker); +} + bool ModelChecker::should_terminate_execution() { /* Infeasible -> don't take any more steps */ @@ -364,6 +372,10 @@ void ModelChecker::do_restart() execution_number = 1; } +void ModelChecker::startMainThread() { + init_thread->setContext(); +} + /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { @@ -371,7 +383,7 @@ void ModelChecker::run() char random_state[256]; initstate(423121, random_state, sizeof(random_state)); - for(int exec = 0;exec < params.maxexecutions;exec ++) { + for(int exec = 0;exec < params.maxexecutions;exec++) { Thread * t = init_thread; do { diff --git a/model.h b/model.h index 8983d017..1269e76e 100644 --- a/model.h +++ b/model.h @@ -64,7 +64,8 @@ public: model_params params; void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); } void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; } - + void startMainThread(); + void startChecker(); MEMALLOC private: /** Flag indicates whether to restart the model checker. */ @@ -107,5 +108,4 @@ private: }; extern ModelChecker *model; -extern bool modelchecker_started; #endif /* __MODEL_H__ */ diff --git a/pthread.cc b/pthread.cc index 808aa207..9a222b9d 100644 --- a/pthread.cc +++ b/pthread.cc @@ -53,6 +53,7 @@ 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(); + model->startChecker(); } ModelExecution *execution = model->get_execution(); diff --git a/snapshot-interface.h b/snapshot-interface.h index 3e3ad71e..4d27ae04 100644 --- a/snapshot-interface.h +++ b/snapshot-interface.h @@ -5,14 +5,15 @@ #ifndef __SNAPINTERFACE_H #define __SNAPINTERFACE_H +#include typedef unsigned int snapshot_id; - typedef void (*VoidFuncPtr)(); + void snapshot_system_init(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, unsigned int numheappages); -void startExecution(VoidFuncPtr entryPoint); +void startExecution(ucontext_t * context, 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 5c1c1e25..2901be3c 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -181,9 +181,9 @@ static void mprot_snapshot_init(unsigned int numbackingpages, snapshot_add_memory_region(pagealignedbase, numheappages); } - -static void mprot_startExecution(VoidFuncPtr entryPoint) { - entryPoint(); +static void mprot_startExecution(ucontext_t * context, VoidFuncPtr entryPoint) { + /* setup the shared-stack context */ + create_context(context, fork_snap->mStackBase, model_calloc(STACK_SIZE_DEFAULT, 1), STACK_SIZE_DEFAULT, entryPoint); } static void mprot_add_to_snapshot(void *addr, unsigned int numPages) @@ -323,6 +323,7 @@ static void create_context(ucontext_t *ctxt, void *stack, size_t stacksize, getcontext(ctxt); ctxt->uc_stack.ss_sp = stack; ctxt->uc_stack.ss_size = stacksize; + ctxt->uc_link = NULL; makecontext(ctxt, func, 0); } @@ -330,7 +331,7 @@ static void create_context(ucontext_t *ctxt, void *stack, size_t stacksize, * process */ static void fork_exit() { - /* Intentionally empty */ + _Exit(EXIT_SUCCESS); } static void createSharedMemory() @@ -376,17 +377,7 @@ static void fork_snapshot_init(unsigned int numbackingpages, 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); - - /* setup the shared-stack context */ - create_context(&fork_snap->shared_ctxt, fork_snap->mStackBase, - STACK_SIZE_DEFAULT, entryPoint); - /* switch to a new entryPoint context, on a new stack */ - model_swapcontext(&private_ctxt, &fork_snap->shared_ctxt); - +static void fork_loop() { /* switch back here when takesnapshot is called */ snapshotid = fork_snap->currSnapShotID; if (model->params.nofork) { @@ -419,8 +410,18 @@ static void fork_startExecution(VoidFuncPtr entryPoint) { } } -static snapshot_id fork_take_snapshot() -{ +static void fork_startExecution(ucontext_t *context, VoidFuncPtr entryPoint) { + /* setup an "exiting" context */ + char stack[128]; + create_context(&exit_ctxt, stack, sizeof(stack), fork_exit); + + /* setup the system context */ + create_context(context, fork_snap->mStackBase, STACK_SIZE_DEFAULT, entryPoint); + /* switch to a new entryPoint context, on a new stack */ + create_context(&private_ctxt, snapshot_calloc(STACK_SIZE_DEFAULT, 1), STACK_SIZE_DEFAULT, fork_loop); +} + +static snapshot_id fork_take_snapshot() { model_swapcontext(&fork_snap->shared_ctxt, &private_ctxt); DEBUG("TAKESNAPSHOT RETURN\n"); return snapshotid; @@ -451,12 +452,12 @@ void snapshot_system_init(unsigned int numbackingpages, #endif } -void startExecution(VoidFuncPtr entryPoint) +void startExecution(ucontext_t *context, VoidFuncPtr entryPoint) { #if USE_MPROTECT_SNAPSHOT - mprot_startExecution(entryPoint); + mprot_startExecution(context, entryPoint); #else - fork_startExecution(entryPoint); + fork_startExecution(context, entryPoint); #endif } diff --git a/threads-model.h b/threads-model.h index 61e3569b..513142b5 100644 --- a/threads-model.h +++ b/threads-model.h @@ -50,6 +50,7 @@ public: static int swap(ucontext_t *ctxt, Thread *t); static int swap(Thread *t, ucontext_t *ctxt); + void setContext(); thread_state get_state() const { return state; } void set_state(thread_state s); thread_id_t get_id() const; diff --git a/threads.cc b/threads.cc index 67f681ca..56942f5f 100644 --- a/threads.cc +++ b/threads.cc @@ -86,6 +86,11 @@ int Thread::create_context() return 0; } +void Thread::setContext() { + set_state(THREAD_RUNNING); + setcontext(&context); +} + /** * Swaps the current context to another thread of execution. This form switches * from a user Thread to a system context.