cmodelint.cc

   1 #include <stdio.h>
   2 #include "model.h"
   3 #include "execution.h"
   4 #include "action.h"
   5 #include "cmodelint.h"
   6 #include "snapshot-interface.h"
   7 #include "threads-model.h"
   8
   9 memory_order orders[6] = {
  10         memory_order_relaxed, memory_order_consume, memory_order_acquire,
  11         memory_order_release, memory_order_acq_rel, memory_order_seq_cst
  12 };
  13
  14 #define ensureModel(action) \
  15         if (!modelchecker_started) {                  \
  16                 if (!model) { \
  17                         snapshot_system_init(10000, 1024, 1024, 40000); \
  18                         model = new ModelChecker(); \
  19                 } \
  20                 model->get_execution()->check_current_action(action); \
  21         }else { \
  22                 model->switch_to_master(action); \
  23         }
  24
  25
  26 #define ensureModelValue(action, type)          \
  27         if (!modelchecker_started) { \
  28                 if (!model) { \
  29                         snapshot_system_init(10000, 1024, 1024, 40000); \
  30                         model = new ModelChecker(); \
  31                 } \
  32                 model->get_execution()->check_current_action(action); \
  33                 return (type) thread_current()->get_return_value();   \
  34         } else { \
  35                 return (type) model->switch_to_master(action);        \
  36         }
  37
  38 /** Performs a read action.*/
  39 uint64_t model_read_action(void * obj, memory_order ord) {
  40         return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
  41 }
  42
  43 /** Performs a write action.*/
  44 void model_write_action(void * obj, memory_order ord, uint64_t val) {
  45         model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val));
  46 }
  47
  48 /** Performs an init action. */
  49 void model_init_action(void * obj, uint64_t val) {
  50         model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
  51 }
  52
  53 /**
  54  * Performs the read part of a RMW action. The next action must either be the
  55  * write part of the RMW action or an explicit close out of the RMW action w/o
  56  * a write.
  57  */
  58 uint64_t model_rmwr_action(void *obj, memory_order ord) {
  59         return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
  60 }
  61
  62 /**
  63  * Performs the read part of a RMW CAS action. The next action must
  64  * either be the write part of the RMW action or an explicit close out
  65  * of the RMW action w/o a write.
  66  */
  67 uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) {
  68         return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size));
  69 }
  70
  71
  72 /** Performs the write part of a RMW action. */
  73 void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
  74         model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
  75 }
  76
  77 /** Closes out a RMW action without doing a write. */
  78 void model_rmwc_action(void *obj, memory_order ord) {
  79         model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
  80 }
  81
  82 /** Issues a fence operation. */
  83 void model_fence_action(memory_order ord) {
  84         model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
  85 }
  86
  87 /* ---  helper functions --- */
  88 uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
  89         ensureModelValue(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj), uint64_t);
  90 }
  91
  92 uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
  93         ensureModelValue(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj), uint64_t);
  94 }
  95
  96 void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) {
  97         ensureModel(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val));
  98 }
  99
 100 void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) {
 101         ensureModel(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj));
 102 }
 103
 104 // cds atomic inits
 105 void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
 106         ensureModel(
 107                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
 108                 );
 109 }
 110 void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
 111         ensureModel(
 112                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
 113                 );
 114 }
 115 void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
 116         ensureModel(
 117                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
 118                 );
 119 }
 120 void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
 121         ensureModel(
 122                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
 123                 );
 124 }
 125
 126
 127 // cds atomic loads
 128 uint8_t cds_atomic_load8(void * obj, int atomic_index, const char * position) {
 129         ensureModelValue(
 130                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint8_t);
 131 }
 132 uint16_t cds_atomic_load16(void * obj, int atomic_index, const char * position) {
 133         ensureModelValue(
 134                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint16_t);
 135 }
 136 uint32_t cds_atomic_load32(void * obj, int atomic_index, const char * position) {
 137         ensureModelValue(
 138                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint32_t
 139                 );
 140 }
 141 uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) {
 142         ensureModelValue(
 143                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint64_t);
 144 }
 145
 146 // cds atomic stores
 147 void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
 148         ensureModel(
 149                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
 150                 );
 151 }
 152 void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
 153         ensureModel(
 154                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
 155                 );
 156 }
 157 void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
 158         ensureModel(
 159                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
 160                 );
 161 }
 162 void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
 163         ensureModel(
 164                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
 165                 );
 166 }
 167
 168 #define _ATOMIC_RMW_(__op__, size, addr, val, atomic_index, position)            \
 169         ({                                                                      \
 170                 uint ## size ## _t _old = model_rmwr_action_helper(addr, atomic_index, position);   \
 171                 uint ## size ## _t _copy = _old;                                          \
 172                 uint ## size ## _t _val = val;                                            \
 173                 _copy __op__ _val;                                                    \
 174                 model_rmw_action_helper(addr, (uint64_t) _copy, atomic_index, position);        \
 175                 return _old;                                                          \
 176         })
 177
 178 // cds atomic exchange
 179 uint8_t cds_atomic_exchange8(void* addr, uint8_t val, int atomic_index, const char * position) {
 180         _ATOMIC_RMW_( =, 8, addr, val, atomic_index, position);
 181 }
 182 uint16_t cds_atomic_exchange16(void* addr, uint16_t val, int atomic_index, const char * position) {
 183         _ATOMIC_RMW_( =, 16, addr, val, atomic_index, position);
 184 }
 185 uint32_t cds_atomic_exchange32(void* addr, uint32_t val, int atomic_index, const char * position) {
 186         _ATOMIC_RMW_( =, 32, addr, val, atomic_index, position);
 187 }
 188 uint64_t cds_atomic_exchange64(void* addr, uint64_t val, int atomic_index, const char * position) {
 189         _ATOMIC_RMW_( =, 64, addr, val, atomic_index, position);
 190 }
 191
 192 // cds atomic fetch add
 193 uint8_t cds_atomic_fetch_add8(void* addr, uint8_t val, int atomic_index, const char * position) {
 194         _ATOMIC_RMW_( +=, 8, addr, val, atomic_index, position);
 195 }
 196 uint16_t cds_atomic_fetch_add16(void* addr, uint16_t val, int atomic_index, const char * position) {
 197         _ATOMIC_RMW_( +=, 16, addr, val, atomic_index, position);
 198 }
 199 uint32_t cds_atomic_fetch_add32(void* addr, uint32_t val, int atomic_index, const char * position) {
 200         _ATOMIC_RMW_( +=, 32, addr, val, atomic_index, position);
 201 }
 202 uint64_t cds_atomic_fetch_add64(void* addr, uint64_t val, int atomic_index, const char * position) {
 203         _ATOMIC_RMW_( +=, 64, addr, val, atomic_index, position);
 204 }
 205
 206 // cds atomic fetch sub
 207 uint8_t cds_atomic_fetch_sub8(void* addr, uint8_t val, int atomic_index, const char * position) {
 208         _ATOMIC_RMW_( -=, 8, addr, val, atomic_index, position);
 209 }
 210 uint16_t cds_atomic_fetch_sub16(void* addr, uint16_t val, int atomic_index, const char * position) {
 211         _ATOMIC_RMW_( -=, 16, addr, val, atomic_index, position);
 212 }
 213 uint32_t cds_atomic_fetch_sub32(void* addr, uint32_t val, int atomic_index, const char * position) {
 214         _ATOMIC_RMW_( -=, 32, addr, val, atomic_index, position);
 215 }
 216 uint64_t cds_atomic_fetch_sub64(void* addr, uint64_t val, int atomic_index, const char * position) {
 217         _ATOMIC_RMW_( -=, 64, addr, val, atomic_index, position);
 218 }
 219
 220 // cds atomic fetch and
 221 uint8_t cds_atomic_fetch_and8(void* addr, uint8_t val, int atomic_index, const char * position) {
 222         _ATOMIC_RMW_( &=, 8, addr, val, atomic_index, position);
 223 }
 224 uint16_t cds_atomic_fetch_and16(void* addr, uint16_t val, int atomic_index, const char * position) {
 225         _ATOMIC_RMW_( &=, 16, addr, val, atomic_index, position);
 226 }
 227 uint32_t cds_atomic_fetch_and32(void* addr, uint32_t val, int atomic_index, const char * position) {
 228         _ATOMIC_RMW_( &=, 32, addr, val, atomic_index, position);
 229 }
 230 uint64_t cds_atomic_fetch_and64(void* addr, uint64_t val, int atomic_index, const char * position) {
 231         _ATOMIC_RMW_( &=, 64, addr, val, atomic_index, position);
 232 }
 233
 234 // cds atomic fetch or
 235 uint8_t cds_atomic_fetch_or8(void* addr, uint8_t val, int atomic_index, const char * position) {
 236         _ATOMIC_RMW_( |=, 8, addr, val, atomic_index, position);
 237 }
 238 uint16_t cds_atomic_fetch_or16(void* addr, uint16_t val, int atomic_index, const char * position) {
 239         _ATOMIC_RMW_( |=, 16, addr, val, atomic_index, position);
 240 }
 241 uint32_t cds_atomic_fetch_or32(void* addr, uint32_t val, int atomic_index, const char * position) {
 242         _ATOMIC_RMW_( |=, 32, addr, val, atomic_index, position);
 243 }
 244 uint64_t cds_atomic_fetch_or64(void* addr, uint64_t val, int atomic_index, const char * position) {
 245         _ATOMIC_RMW_( |=, 64, addr, val, atomic_index, position);
 246 }
 247
 248 // cds atomic fetch xor
 249 uint8_t cds_atomic_fetch_xor8(void* addr, uint8_t val, int atomic_index, const char * position) {
 250         _ATOMIC_RMW_( ^=, 8, addr, val, atomic_index, position);
 251 }
 252 uint16_t cds_atomic_fetch_xor16(void* addr, uint16_t val, int atomic_index, const char * position) {
 253         _ATOMIC_RMW_( ^=, 16, addr, val, atomic_index, position);
 254 }
 255 uint32_t cds_atomic_fetch_xor32(void* addr, uint32_t val, int atomic_index, const char * position) {
 256         _ATOMIC_RMW_( ^=, 32, addr, val, atomic_index, position);
 257 }
 258 uint64_t cds_atomic_fetch_xor64(void* addr, uint64_t val, int atomic_index, const char * position) {
 259         _ATOMIC_RMW_( ^=, 64, addr, val, atomic_index, position);
 260 }
 261
 262 // cds atomic compare and exchange
 263 // In order to accomodate the LLVM PASS, the return values are not true or false.
 264
 265 #define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_
 266 #define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index, position)                            \
 267         ({                                                                                              \
 268                 uint ## size ## _t _desired = desired;                                                            \
 269                 uint ## size ## _t _expected = expected;                                                          \
 270                 uint ## size ## _t _old = model_rmwrcas_action_helper(addr, atomic_index, _expected, sizeof(_expected), position); \
 271                 if (_old == _expected) {                                                                    \
 272                         model_rmw_action_helper(addr, (uint64_t) _desired, atomic_index, position); return _expected; }      \
 273                 else {                                                                                        \
 274                         model_rmwc_action_helper(addr, atomic_index, position); _expected = _old; return _old; }              \
 275         })
 276
 277 // atomic_compare_exchange version 1: the CmpOperand (corresponds to expected)
 278 // extracted from LLVM IR is an integer type.
 279
 280 uint8_t cds_atomic_compare_exchange8_v1(void* addr, uint8_t expected, uint8_t desired,
 281                                                                                                                                                                 int atomic_index_succ, int atomic_index_fail, const char *position )
 282 {
 283         _ATOMIC_CMPSWP_(8, addr, expected, desired,
 284                                                                         atomic_index_succ, position);
 285 }
 286 uint16_t cds_atomic_compare_exchange16_v1(void* addr, uint16_t expected, uint16_t desired,
 287                                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 288 {
 289         _ATOMIC_CMPSWP_(16, addr, expected, desired,
 290                                                                         atomic_index_succ, position);
 291 }
 292 uint32_t cds_atomic_compare_exchange32_v1(void* addr, uint32_t expected, uint32_t desired,
 293                                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 294 {
 295         _ATOMIC_CMPSWP_(32, addr, expected, desired,
 296                                                                         atomic_index_succ, position);
 297 }
 298 uint64_t cds_atomic_compare_exchange64_v1(void* addr, uint64_t expected, uint64_t desired,
 299                                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 300 {
 301         _ATOMIC_CMPSWP_(64, addr, expected, desired,
 302                                                                         atomic_index_succ, position);
 303 }
 304
 305 // atomic_compare_exchange version 2
 306 bool cds_atomic_compare_exchange8_v2(void* addr, uint8_t* expected, uint8_t desired,
 307                                                                                                                                                  int atomic_index_succ, int atomic_index_fail, const char *position )
 308 {
 309         uint8_t ret = cds_atomic_compare_exchange8_v1(addr, *expected,
 310                                                                                                                                                                                                 desired, atomic_index_succ, atomic_index_fail, position);
 311         if (ret == *expected) return true;
 312         else return false;
 313 }
 314 bool cds_atomic_compare_exchange16_v2(void* addr, uint16_t* expected, uint16_t desired,
 315                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 316 {
 317         uint16_t ret = cds_atomic_compare_exchange16_v1(addr, *expected,
 318                                                                                                                                                                                                         desired, atomic_index_succ, atomic_index_fail, position);
 319         if (ret == *expected) return true;
 320         else return false;
 321 }
 322 bool cds_atomic_compare_exchange32_v2(void* addr, uint32_t* expected, uint32_t desired,
 323                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 324 {
 325         uint32_t ret = cds_atomic_compare_exchange32_v1(addr, *expected,
 326                                                                                                                                                                                                         desired, atomic_index_succ, atomic_index_fail, position);
 327         if (ret == *expected) return true;
 328         else return false;
 329 }
 330 bool cds_atomic_compare_exchange64_v2(void* addr, uint64_t* expected, uint64_t desired,
 331                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 332 {
 333         uint64_t ret = cds_atomic_compare_exchange64_v1(addr, *expected,
 334                                                                                                                                                                                                         desired, atomic_index_succ, atomic_index_fail, position);
 335         if (ret == *expected) return true;
 336         else return false;
 337 }
 338
 339
 340 // cds atomic thread fence
 341
 342 void cds_atomic_thread_fence(int atomic_index, const char * position) {
 343         model->switch_to_master(
 344                 new ModelAction(ATOMIC_FENCE, position, orders[atomic_index], FENCE_LOCATION)
 345                 );
 346 }
 347
 348 /*
 349  #define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ )                         \
 350         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
 351                 __typeof__(__e__) __q__ = (__e__);                            \
 352                 __typeof__(__m__) __v__ = (__m__);                            \
 353                 bool __r__;                                                   \
 354                 __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
 355                 if (__t__ == * __q__ ) {                                      \
 356                         model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
 357                 else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
 358                 __r__; })
 359
 360  #define _ATOMIC_FENCE_( __x__ ) \
 361         ({ model_fence_action(__x__);})
 362  */
 363
 364 /*
 365
 366  #define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ )                         \
 367         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
 368         __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
 369         __typeof__(__m__) __v__ = (__m__);                                    \
 370         __typeof__((__a__)->__f__) __copy__= __old__;                         \
 371         __copy__ __o__ __v__;                                                 \
 372         model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);          \
 373         __old__ = __old__;  Silence clang (-Wunused-value)                    \
 374          })
 375  */