X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=cmodelint.cc;h=9f1c9c0616d20cb7c85c5e9b90567cd70596660d;hp=9faae5345e857caa7918b278527ba713c9259ef8;hb=refs%2Fheads%2Fvagrant;hpb=c76be793b17d234cc803f89bdda90c89f57ce17e diff --git a/cmodelint.cc b/cmodelint.cc index 9faae534..9f1c9c06 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -4,7 +4,6 @@ #include "model.h" #include "execution.h" #include "action.h" -#include "history.h" #include "cmodelint.h" #include "snapshot-interface.h" #include "threads-model.h" @@ -12,96 +11,68 @@ memory_order orders[6] = { memory_order_relaxed, memory_order_consume, memory_order_acquire, - memory_order_release, memory_order_acq_rel, memory_order_seq_cst + 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) { \ + createModelIfNotExist(); \ + return (uint ## size ## _t)model->switch_thread(new ModelAction(ATOMIC_READ, position, memory_order_volatile_load, obj)); \ + } + +VOLATILELOAD(8) +VOLATILELOAD(16) +VOLATILELOAD(32) +VOLATILELOAD(64) + +// cds volatile stores +#define VOLATILESTORE(size) \ + void cds_volatile_store ## size (void * obj, uint ## size ## _t val, const char * position) { \ + 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_id(); \ + for(int i=0;i < size / 8;i++) { \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ + } \ + } + +VOLATILESTORE(8) +VOLATILESTORE(16) +VOLATILESTORE(32) +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)); \ - *((uint ## size ## _t *)obj) = val; \ - thread_id_t tid = thread_current()->get_id(); \ + 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_id(); \ for(int i=0;i < size / 8;i++) { \ - recordWrite(tid, (void *)(((char *)obj)+i)); \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ } @@ -113,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) @@ -126,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)); \ - *((uint ## size ## _t *)obj) = val; \ - thread_id_t tid = thread_current()->get_id(); \ + 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_id(); \ for(int i=0;i < size / 8;i++) { \ - recordWrite(tid, (void *)(((char *)obj)+i)); \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ } @@ -148,12 +124,13 @@ CDSATOMICSTORE(64) uint ## size ## _t _val = val; \ _copy __op__ _val; \ model_rmw_action_helper(addr, (uint64_t) _copy, atomic_index, position); \ - *((uint ## size ## _t *)addr) = _copy; \ - thread_id_t tid = thread_current()->get_id(); \ + *((volatile uint ## size ## _t *)addr) = _copy; \ + 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 @@ -233,8 +210,8 @@ CDSATOMICXOR(64) uint ## size ## _t _old = model_rmwrcas_action_helper(addr, atomic_index, _expected, sizeof(_expected), position); \ if (_old == _expected) { \ model_rmw_action_helper(addr, (uint64_t) _desired, atomic_index, position); \ - *((uint ## size ## _t *)addr) = desired; \ - thread_id_t tid = thread_current()->get_id(); \ + *((volatile uint ## size ## _t *)addr) = desired; \ + thread_id_t tid = thread_current_id(); \ for(int i=0;i < size / 8;i++) { \ recordWrite(tid, (void *)(((char *)addr)+i)); \ } \ @@ -270,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) ); } @@ -305,45 +282,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) { */ void cds_func_entry(const char * funcName) { - if (!model) return; - - 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) { - if (!model) return; - - 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()); }