X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=cmodelint.cc;h=9f1c9c0616d20cb7c85c5e9b90567cd70596660d;hb=HEAD;hp=fdac33aa1324d5735cd96f09ab2b712a9a53119f;hpb=6898da1b7c46ddf3427ea0127dc68f8cc6016511;p=c11tester.git diff --git a/cmodelint.cc b/cmodelint.cc index fdac33aa..9f1c9c06 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -4,100 +4,42 @@ #include "model.h" #include "execution.h" #include "action.h" -#include "history.h" #include "cmodelint.h" #include "snapshot-interface.h" #include "threads-model.h" #include "datarace.h" -memory_order orders[8] = { +memory_order orders[6] = { memory_order_relaxed, memory_order_consume, memory_order_acquire, 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(); - model->startChecker(); - } -} - -/** 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)); -} - -/** Performs a write action.*/ -void model_write_action(void * obj, memory_order ord, uint64_t val) { - model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val)); -} - -/** Performs an init action. */ -void model_init_action(void * obj, uint64_t val) { - model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val)); -} - -/** - * Performs the read part of a RMW action. The next action must either be the - * write part of the RMW action or an explicit close out of the RMW action w/o - * a write. - */ -uint64_t model_rmwr_action(void *obj, memory_order ord) { - return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj)); -} - -/** - * Performs the read part of a RMW CAS action. The next action must - * either be the write part of the RMW action or an explicit close out - * of the RMW action w/o a write. - */ -uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) { - return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size)); -} - - -/** Performs the write part of a RMW action. */ -void model_rmw_action(void *obj, memory_order ord, uint64_t val) { - model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val)); -} - -/** Closes out a RMW action without doing a write. */ -void model_rmwc_action(void *obj, memory_order ord) { - model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj)); -} - -/** Issues a fence operation. */ -void model_fence_action(memory_order ord) { - model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION)); -} - /* --- helper functions --- */ uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) { - ensureModel(); - return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size)); + createModelIfNotExist(); + return model->switch_thread(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) { - ensureModel(); - return model->switch_to_master(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)); + createModelIfNotExist(); + return model->switch_thread(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(); - model->switch_to_master(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)); + createModelIfNotExist(); + model->switch_thread(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)); } void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) { - ensureModel(); - model->switch_to_master(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)); + createModelIfNotExist(); + model->switch_thread(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)); } // cds volatile loads #define VOLATILELOAD(size) \ uint ## size ## _t cds_volatile_load ## size(void * obj, const char * position) { \ - ensureModel(); \ - return (uint ## size ## _t)model->switch_to_master(new ModelAction(ATOMIC_READ, position, memory_order_relaxed, obj)); \ + createModelIfNotExist(); \ + return (uint ## size ## _t)model->switch_thread(new ModelAction(ATOMIC_READ, position, memory_order_volatile_load, obj)); \ } VOLATILELOAD(8) @@ -108,12 +50,12 @@ VOLATILELOAD(64) // cds volatile stores #define VOLATILESTORE(size) \ void cds_volatile_store ## size (void * obj, uint ## size ## _t val, const char * position) { \ - ensureModel(); \ - model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, memory_order_relaxed, obj, (uint64_t) val)); \ + createModelIfNotExist(); \ + model->switch_thread(new ModelAction(ATOMIC_WRITE, position, memory_order_volatile_store, obj, (uint64_t) val)); \ *((volatile uint ## size ## _t *)obj) = val; \ - thread_id_t tid = thread_current()->get_id(); \ + thread_id_t tid = thread_current_id(); \ for(int i=0;i < size / 8;i++) { \ - recordWrite(tid, (void *)(((char *)obj)+i)); \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ } @@ -125,12 +67,12 @@ VOLATILESTORE(64) // cds atomic inits #define CDSATOMICINT(size) \ void cds_atomic_init ## size (void * obj, uint ## size ## _t val, const char * position) { \ - ensureModel(); \ - model->switch_to_master(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)); \ + createModelIfNotExist(); \ + model->switch_thread(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)); \ *((volatile uint ## size ## _t *)obj) = val; \ - thread_id_t tid = thread_current()->get_id(); \ + thread_id_t tid = thread_current_id(); \ for(int i=0;i < size / 8;i++) { \ - recordWrite(tid, (void *)(((char *)obj)+i)); \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ } @@ -142,9 +84,14 @@ CDSATOMICINT(64) // cds atomic loads #define CDSATOMICLOAD(size) \ uint ## size ## _t cds_atomic_load ## size(void * obj, int atomic_index, const char * position) { \ - ensureModel(); \ - return (uint ## size ## _t)model->switch_to_master( \ + createModelIfNotExist(); \ + uint ## size ## _t val = (uint ## size ## _t)model->switch_thread( \ new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)); \ + thread_id_t tid = thread_current_id(); \ + for(int i=0;i < size / 8;i++) { \ + atomraceCheckRead(tid, (void *)(((char *)obj)+i)); \ + } \ + return val; \ } CDSATOMICLOAD(8) @@ -155,12 +102,12 @@ CDSATOMICLOAD(64) // cds atomic stores #define CDSATOMICSTORE(size) \ void cds_atomic_store ## size(void * obj, uint ## size ## _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)); \ + createModelIfNotExist(); \ + model->switch_thread(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)); \ *((volatile uint ## size ## _t *)obj) = val; \ - thread_id_t tid = thread_current()->get_id(); \ + thread_id_t tid = thread_current_id(); \ for(int i=0;i < size / 8;i++) { \ - recordWrite(tid, (void *)(((char *)obj)+i)); \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ } @@ -178,11 +125,12 @@ CDSATOMICSTORE(64) _copy __op__ _val; \ model_rmw_action_helper(addr, (uint64_t) _copy, atomic_index, position); \ *((volatile uint ## size ## _t *)addr) = _copy; \ - thread_id_t tid = thread_current()->get_id(); \ + thread_id_t tid = thread_current_id(); \ for(int i=0;i < size / 8;i++) { \ + atomraceCheckRead(tid, (void *)(((char *)addr)+i)); \ recordWrite(tid, (void *)(((char *)addr)+i)); \ } \ - return _old; \ + return _old; \ }) // cds atomic exchange @@ -263,7 +211,7 @@ CDSATOMICXOR(64) if (_old == _expected) { \ model_rmw_action_helper(addr, (uint64_t) _desired, atomic_index, position); \ *((volatile uint ## size ## _t *)addr) = desired; \ - thread_id_t tid = thread_current()->get_id(); \ + thread_id_t tid = thread_current_id(); \ for(int i=0;i < size / 8;i++) { \ recordWrite(tid, (void *)(((char *)addr)+i)); \ } \ @@ -299,7 +247,7 @@ CDSATOMICCASV2(64) // cds atomic thread fence void cds_atomic_thread_fence(int atomic_index, const char * position) { - model->switch_to_master( + model->switch_thread( new ModelAction(ATOMIC_FENCE, position, orders[atomic_index], FENCE_LOCATION) ); } @@ -334,43 +282,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) { */ void cds_func_entry(const char * funcName) { - ensureModel(); - Thread * th = thread_current(); - uint32_t func_id; - - ModelHistory *history = model->get_history(); - if ( !history->getFuncMap()->contains(funcName) ) { - // add func id to func map - func_id = history->get_func_counter(); - history->incr_func_counter(); - history->getFuncMap()->put(funcName, func_id); - - // add func id to reverse func map - ModelVector * func_map_rev = history->getFuncMapRev(); - if ( func_map_rev->size() <= func_id ) - func_map_rev->resize( func_id + 1 ); - func_map_rev->at(func_id) = funcName; - } else { - func_id = history->getFuncMap()->get(funcName); - } - - history->enter_function(func_id, th->get_id()); } void cds_func_exit(const char * funcName) { - ensureModel(); - Thread * th = thread_current(); - uint32_t func_id; - - ModelHistory *history = model->get_history(); - func_id = history->getFuncMap()->get(funcName); - - /* func_id not found; this could happen in the case where a function calls cds_func_entry - * when the model has been defined yet, but then an atomic inside the function initializes - * the model. And then cds_func_exit is called upon the function exiting. - */ - if (func_id == 0) - return; - - history->exit_function(func_id, th->get_id()); }