X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=cmodelint.cc;h=fdac33aa1324d5735cd96f09ab2b712a9a53119f;hb=6898da1b7c46ddf3427ea0127dc68f8cc6016511;hp=c052552ed5936779fba36e52538c0627e417b9c9;hpb=b19bfef4c4ef886d028e79559bb40fde2189796d;p=c11tester.git diff --git a/cmodelint.cc b/cmodelint.cc index c052552e..fdac33aa 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -8,10 +8,11 @@ #include "cmodelint.h" #include "snapshot-interface.h" #include "threads-model.h" +#include "datarace.h" -memory_order orders[6] = { +memory_order orders[8] = { 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() { @@ -92,12 +93,45 @@ void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) model->switch_to_master(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)); \ + } + +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) { \ + ensureModel(); \ + model->switch_to_master(new ModelAction(ATOMIC_WRITE, 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)); \ + } \ + } + +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; \ + *((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)); \ + } \ } CDSATOMICINT(8) @@ -109,7 +143,7 @@ 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( \ + return (uint ## size ## _t)model->switch_to_master( \ new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)); \ } @@ -119,12 +153,15 @@ CDSATOMICLOAD(32) 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; \ + *((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)); \ + } \ } CDSATOMICSTORE(8) @@ -140,6 +177,11 @@ CDSATOMICSTORE(64) uint ## size ## _t _val = val; \ _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(); \ + for(int i=0;i < size / 8;i++) { \ + recordWrite(tid, (void *)(((char *)addr)+i)); \ + } \ return _old; \ }) @@ -219,7 +261,13 @@ CDSATOMICXOR(64) uint ## size ## _t _expected = expected; \ 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); return _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(); \ + for(int i=0;i < size / 8;i++) { \ + recordWrite(tid, (void *)(((char *)addr)+i)); \ + } \ + return _expected; } \ else { \ model_rmwc_action_helper(addr, atomic_index, position); _expected = _old; return _old; } \ }) @@ -286,8 +334,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) { */ void cds_func_entry(const char * funcName) { - if (!model) return; - + ensureModel(); Thread * th = thread_current(); uint32_t func_id; @@ -311,8 +358,7 @@ void cds_func_entry(const char * funcName) { } void cds_func_exit(const char * funcName) { - if (!model) return; - + ensureModel(); Thread * th = thread_current(); uint32_t func_id;