X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=cmodelint.cc;h=fe91d5373583bd337b5f2d8022f97e945243d216;hp=b39e15b31e4ca7dfc27c870c9145bc1526aceee7;hb=055fb927ea688ec513508b0821e331558eea40d1;hpb=11349f4e83c1446d5c678384a7d45e410c82c3e2 diff --git a/cmodelint.cc b/cmodelint.cc index b39e15b3..fe91d537 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -10,7 +10,7 @@ #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, }; @@ -23,81 +23,32 @@ static void ensureModel() { } } -/** 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)); + 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)); + 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)); + 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)); + 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)); \ + return (uint ## size ## _t)model->switch_thread(new ModelAction(ATOMIC_READ, position, memory_order_volatile_load, obj)); \ } VOLATILELOAD(8) @@ -109,8 +60,12 @@ VOLATILELOAD(64) #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)); \ + 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(); \ + for(int i=0;i < size / 8;i++) { \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ + } \ } VOLATILESTORE(8) @@ -122,11 +77,11 @@ VOLATILESTORE(64) #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)); \ + 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(); \ for(int i=0;i < size / 8;i++) { \ - recordWrite(tid, (void *)(((char *)obj)+i)); \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ } @@ -139,8 +94,13 @@ CDSATOMICINT(64) #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( \ + 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()->get_id(); \ + for(int i=0;i < size / 8;i++) { \ + atomraceCheckRead(tid, (void *)(((char *)obj)+i)); \ + } \ + return val; \ } CDSATOMICLOAD(8) @@ -152,11 +112,11 @@ CDSATOMICLOAD(64) #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)); \ + 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(); \ for(int i=0;i < size / 8;i++) { \ - recordWrite(tid, (void *)(((char *)obj)+i)); \ + atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ } @@ -176,9 +136,10 @@ CDSATOMICSTORE(64) *((volatile uint ## size ## _t *)addr) = _copy; \ thread_id_t tid = thread_current()->get_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 @@ -295,7 +256,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) ); } @@ -330,8 +291,8 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) { */ void cds_func_entry(const char * funcName) { - if (!model) return; - +#ifdef NEWFUZZER + ensureModel(); Thread * th = thread_current(); uint32_t func_id; @@ -346,29 +307,34 @@ void cds_func_entry(const char * funcName) { 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()); +#endif } void cds_func_exit(const char * funcName) { - if (!model) return; +#ifdef NEWFUZZER + 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. - */ +/* + * 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()); +#endif }