X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=cmodelint.cc;h=9f1c9c0616d20cb7c85c5e9b90567cd70596660d;hb=HEAD;hp=1a03153fbeb908fe782a3cce80d7fcb7074ecab5;hpb=69d9b3609ff724140893c7dffb1e7a38c3090a81;p=c11tester.git diff --git a/cmodelint.cc b/cmodelint.cc index 1a03153f..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[7] = { +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,10 +50,10 @@ 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++) { \ atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ @@ -125,10 +67,10 @@ 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++) { \ atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ @@ -142,10 +84,10 @@ CDSATOMICINT(64) // cds atomic loads #define CDSATOMICLOAD(size) \ uint ## size ## _t cds_atomic_load ## size(void * obj, int atomic_index, const char * position) { \ - ensureModel(); \ - uint ## size ## _t val = (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()->get_id(); \ + thread_id_t tid = thread_current_id(); \ for(int i=0;i < size / 8;i++) { \ atomraceCheckRead(tid, (void *)(((char *)obj)+i)); \ } \ @@ -160,10 +102,10 @@ 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++) { \ atomraceCheckWrite(tid, (void *)(((char *)obj)+i)); \ } \ @@ -183,7 +125,7 @@ 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)); \ @@ -269,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)); \ } \ @@ -305,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) ); } @@ -340,47 +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()); - */ }