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         return model->switch_to_master(
  90                 new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj)
  91                 );
  92 }
  93
  94 uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
  95         return model->switch_to_master(
  96                 new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)
  97                 );
  98 }
  99
 100 void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) {
 101         model->switch_to_master(
 102                 new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)
 103                 );
 104 }
 105
 106 void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) {
 107         model->switch_to_master(
 108                 new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)
 109                 );
 110 }
 111
 112 // cds atomic inits
 113 void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
 114         ensureModel(
 115                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
 116                 );
 117 }
 118 void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
 119         ensureModel(
 120                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
 121                 );
 122 }
 123 void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
 124         ensureModel(
 125                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
 126                 );
 127 }
 128 void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
 129         ensureModel(
 130                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
 131                 );
 132 }
 133
 134
 135 // cds atomic loads
 136 uint8_t cds_atomic_load8(void * obj, int atomic_index, const char * position) {
 137         ensureModelValue(
 138                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint8_t);
 139 }
 140 uint16_t cds_atomic_load16(void * obj, int atomic_index, const char * position) {
 141         ensureModelValue(
 142                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint16_t);
 143 }
 144 uint32_t cds_atomic_load32(void * obj, int atomic_index, const char * position) {
 145         ensureModelValue(
 146                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint32_t
 147                 );
 148 }
 149 uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) {
 150         ensureModelValue(
 151                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint64_t);
 152 }
 153
 154 // cds atomic stores
 155 void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
 156         ensureModel(
 157                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
 158                 );
 159 }
 160 void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
 161         ensureModel(
 162                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
 163                 );
 164 }
 165 void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
 166         ensureModel(
 167                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
 168                 );
 169 }
 170 void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
 171         ensureModel(
 172                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
 173                 );
 174 }
 175
 176 #define _ATOMIC_RMW_(__op__, size, addr, val, atomic_index, position)            \
 177         ({                                                                      \
 178                 uint ## size ## _t _old = model_rmwr_action_helper(addr, atomic_index, position);   \
 179                 uint ## size ## _t _copy = _old;                                          \
 180                 uint ## size ## _t _val = val;                                            \
 181                 _copy __op__ _val;                                                    \
 182                 model_rmw_action_helper(addr, (uint64_t) _copy, atomic_index, position);        \
 183                 return _old;                                                          \
 184         })
 185
 186 // cds atomic exchange
 187 uint8_t cds_atomic_exchange8(void* addr, uint8_t val, int atomic_index, const char * position) {
 188         _ATOMIC_RMW_( =, 8, addr, val, atomic_index, position);
 189 }
 190 uint16_t cds_atomic_exchange16(void* addr, uint16_t val, int atomic_index, const char * position) {
 191         _ATOMIC_RMW_( =, 16, addr, val, atomic_index, position);
 192 }
 193 uint32_t cds_atomic_exchange32(void* addr, uint32_t val, int atomic_index, const char * position) {
 194         _ATOMIC_RMW_( =, 32, addr, val, atomic_index, position);
 195 }
 196 uint64_t cds_atomic_exchange64(void* addr, uint64_t val, int atomic_index, const char * position) {
 197         _ATOMIC_RMW_( =, 64, addr, val, atomic_index, position);
 198 }
 199
 200 // cds atomic fetch add
 201 uint8_t cds_atomic_fetch_add8(void* addr, uint8_t val, int atomic_index, const char * position) {
 202         _ATOMIC_RMW_( +=, 8, addr, val, atomic_index, position);
 203 }
 204 uint16_t cds_atomic_fetch_add16(void* addr, uint16_t val, int atomic_index, const char * position) {
 205         _ATOMIC_RMW_( +=, 16, addr, val, atomic_index, position);
 206 }
 207 uint32_t cds_atomic_fetch_add32(void* addr, uint32_t val, int atomic_index, const char * position) {
 208         _ATOMIC_RMW_( +=, 32, addr, val, atomic_index, position);
 209 }
 210 uint64_t cds_atomic_fetch_add64(void* addr, uint64_t val, int atomic_index, const char * position) {
 211         _ATOMIC_RMW_( +=, 64, addr, val, atomic_index, position);
 212 }
 213
 214 // cds atomic fetch sub
 215 uint8_t cds_atomic_fetch_sub8(void* addr, uint8_t val, int atomic_index, const char * position) {
 216         _ATOMIC_RMW_( -=, 8, addr, val, atomic_index, position);
 217 }
 218 uint16_t cds_atomic_fetch_sub16(void* addr, uint16_t val, int atomic_index, const char * position) {
 219         _ATOMIC_RMW_( -=, 16, addr, val, atomic_index, position);
 220 }
 221 uint32_t cds_atomic_fetch_sub32(void* addr, uint32_t val, int atomic_index, const char * position) {
 222         _ATOMIC_RMW_( -=, 32, addr, val, atomic_index, position);
 223 }
 224 uint64_t cds_atomic_fetch_sub64(void* addr, uint64_t val, int atomic_index, const char * position) {
 225         _ATOMIC_RMW_( -=, 64, addr, val, atomic_index, position);
 226 }
 227
 228 // cds atomic fetch and
 229 uint8_t cds_atomic_fetch_and8(void* addr, uint8_t val, int atomic_index, const char * position) {
 230         _ATOMIC_RMW_( &=, 8, addr, val, atomic_index, position);
 231 }
 232 uint16_t cds_atomic_fetch_and16(void* addr, uint16_t val, int atomic_index, const char * position) {
 233         _ATOMIC_RMW_( &=, 16, addr, val, atomic_index, position);
 234 }
 235 uint32_t cds_atomic_fetch_and32(void* addr, uint32_t val, int atomic_index, const char * position) {
 236         _ATOMIC_RMW_( &=, 32, addr, val, atomic_index, position);
 237 }
 238 uint64_t cds_atomic_fetch_and64(void* addr, uint64_t val, int atomic_index, const char * position) {
 239         _ATOMIC_RMW_( &=, 64, addr, val, atomic_index, position);
 240 }
 241
 242 // cds atomic fetch or
 243 uint8_t cds_atomic_fetch_or8(void* addr, uint8_t val, int atomic_index, const char * position) {
 244         _ATOMIC_RMW_( |=, 8, addr, val, atomic_index, position);
 245 }
 246 uint16_t cds_atomic_fetch_or16(void* addr, uint16_t val, int atomic_index, const char * position) {
 247         _ATOMIC_RMW_( |=, 16, addr, val, atomic_index, position);
 248 }
 249 uint32_t cds_atomic_fetch_or32(void* addr, uint32_t val, int atomic_index, const char * position) {
 250         _ATOMIC_RMW_( |=, 32, addr, val, atomic_index, position);
 251 }
 252 uint64_t cds_atomic_fetch_or64(void* addr, uint64_t val, int atomic_index, const char * position) {
 253         _ATOMIC_RMW_( |=, 64, addr, val, atomic_index, position);
 254 }
 255
 256 // cds atomic fetch xor
 257 uint8_t cds_atomic_fetch_xor8(void* addr, uint8_t val, int atomic_index, const char * position) {
 258         _ATOMIC_RMW_( ^=, 8, addr, val, atomic_index, position);
 259 }
 260 uint16_t cds_atomic_fetch_xor16(void* addr, uint16_t val, int atomic_index, const char * position) {
 261         _ATOMIC_RMW_( ^=, 16, addr, val, atomic_index, position);
 262 }
 263 uint32_t cds_atomic_fetch_xor32(void* addr, uint32_t val, int atomic_index, const char * position) {
 264         _ATOMIC_RMW_( ^=, 32, addr, val, atomic_index, position);
 265 }
 266 uint64_t cds_atomic_fetch_xor64(void* addr, uint64_t val, int atomic_index, const char * position) {
 267         _ATOMIC_RMW_( ^=, 64, addr, val, atomic_index, position);
 268 }
 269
 270 // cds atomic compare and exchange
 271 // In order to accomodate the LLVM PASS, the return values are not true or false.
 272
 273 #define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_
 274 #define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index, position)                            \
 275         ({                                                                                              \
 276                 uint ## size ## _t _desired = desired;                                                            \
 277                 uint ## size ## _t _expected = expected;                                                          \
 278                 uint ## size ## _t _old = model_rmwrcas_action_helper(addr, atomic_index, _expected, sizeof(_expected), position); \
 279                 if (_old == _expected) {                                                                    \
 280                         model_rmw_action_helper(addr, (uint64_t) _desired, atomic_index, position); return _expected; }      \
 281                 else {                                                                                        \
 282                         model_rmwc_action_helper(addr, atomic_index, position); _expected = _old; return _old; }              \
 283         })
 284
 285 // atomic_compare_exchange version 1: the CmpOperand (corresponds to expected)
 286 // extracted from LLVM IR is an integer type.
 287
 288 uint8_t cds_atomic_compare_exchange8_v1(void* addr, uint8_t expected, uint8_t desired,
 289                                                                                                                                                                 int atomic_index_succ, int atomic_index_fail, const char *position )
 290 {
 291         _ATOMIC_CMPSWP_(8, addr, expected, desired,
 292                                                                         atomic_index_succ, position);
 293 }
 294 uint16_t cds_atomic_compare_exchange16_v1(void* addr, uint16_t expected, uint16_t desired,
 295                                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 296 {
 297         _ATOMIC_CMPSWP_(16, addr, expected, desired,
 298                                                                         atomic_index_succ, position);
 299 }
 300 uint32_t cds_atomic_compare_exchange32_v1(void* addr, uint32_t expected, uint32_t desired,
 301                                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 302 {
 303         _ATOMIC_CMPSWP_(32, addr, expected, desired,
 304                                                                         atomic_index_succ, position);
 305 }
 306 uint64_t cds_atomic_compare_exchange64_v1(void* addr, uint64_t expected, uint64_t desired,
 307                                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 308 {
 309         _ATOMIC_CMPSWP_(64, addr, expected, desired,
 310                                                                         atomic_index_succ, position);
 311 }
 312
 313 // atomic_compare_exchange version 2
 314 bool cds_atomic_compare_exchange8_v2(void* addr, uint8_t* expected, uint8_t desired,
 315                                                                                                                                                  int atomic_index_succ, int atomic_index_fail, const char *position )
 316 {
 317         uint8_t ret = cds_atomic_compare_exchange8_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_exchange16_v2(void* addr, uint16_t* expected, uint16_t desired,
 323                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 324 {
 325         uint16_t ret = cds_atomic_compare_exchange16_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_exchange32_v2(void* addr, uint32_t* expected, uint32_t desired,
 331                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 332 {
 333         uint32_t ret = cds_atomic_compare_exchange32_v1(addr, *expected,
 334                                                                                                                                                                                                         desired, atomic_index_succ, atomic_index_fail, position);
 335         if (ret == *expected) return true;
 336         else return false;
 337 }
 338 bool cds_atomic_compare_exchange64_v2(void* addr, uint64_t* expected, uint64_t desired,
 339                                                                                                                                                         int atomic_index_succ, int atomic_index_fail, const char *position)
 340 {
 341         uint64_t ret = cds_atomic_compare_exchange64_v1(addr, *expected,
 342                                                                                                                                                                                                         desired, atomic_index_succ, atomic_index_fail, position);
 343         if (ret == *expected) return true;
 344         else return false;
 345 }
 346
 347
 348 // cds atomic thread fence
 349
 350 void cds_atomic_thread_fence(int atomic_index, const char * position) {
 351         model->switch_to_master(
 352                 new ModelAction(ATOMIC_FENCE, position, orders[atomic_index], FENCE_LOCATION)
 353                 );
 354 }
 355
 356 /*
 357  #define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ )                         \
 358         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
 359                 __typeof__(__e__) __q__ = (__e__);                            \
 360                 __typeof__(__m__) __v__ = (__m__);                            \
 361                 bool __r__;                                                   \
 362                 __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
 363                 if (__t__ == * __q__ ) {                                      \
 364                         model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
 365                 else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
 366                 __r__; })
 367
 368  #define _ATOMIC_FENCE_( __x__ ) \
 369         ({ model_fence_action(__x__);})
 370  */
 371
 372 /*
 373
 374  #define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ )                         \
 375         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
 376         __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
 377         __typeof__(__m__) __v__ = (__m__);                                    \
 378         __typeof__((__a__)->__f__) __copy__= __old__;                         \
 379         __copy__ __o__ __v__;                                                 \
 380         model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);          \
 381         __old__ = __old__;  Silence clang (-Wunused-value)                    \
 382          })
 383  */