benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c

   1 #include <stdio.h>
   2 #include <threads.h>
   3 #include <stdlib.h>
   4
   5 #include "libinterface.h"
   6
   7 #define RW_LOCK_BIAS            0x00100000
   8 #define WRITE_LOCK_CMP          RW_LOCK_BIAS
   9
  10 /** Example implementation of linux rw lock along with 2 thread test
  11  *  driver... */
  12
  13 typedef union {
  14         int lock;
  15 } rwlock_t;
  16
  17 static inline void read_lock(MCID _mrw, rwlock_t *rw)
  18 {
  19         MCID _rmw0 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
  20         int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
  21
  22         MC2_enterLoop();
  23         while (true) {
  24                 MCID _br0;
  25
  26                 int _cond0 = priorvalue <= 0;
  27                 MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _rmw0);
  28                 if (_cond0) {_br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
  29
  30                         MC2_merge(_br0);
  31                 } else {
  32                         _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);
  33                         break;
  34                 }
  35
  36                 MCID _rmw1 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
  37                 rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
  38
  39                 MC2_enterLoop();
  40                 while (true) {
  41                         MCID _mstatus; _mstatus=MC2_nextOpLoadOffset(_mrw, MC2_OFFSET(rwlock_t *, lock)); int status = load_32(&rw->lock);
  42                         MCID _br1;
  43
  44                         int _cond1 = status > 0;
  45                         MCID _cond1_m = MC2_function_id(2, 1, sizeof(_cond1), _cond1, _mstatus);
  46                         if (_cond1) {_br1 = MC2_branchUsesID(_cond1_m, 1, 2, true);
  47
  48                                 MC2_merge(_br1);
  49                         } else {
  50                                 _br1 = MC2_branchUsesID(_cond1_m, 0, 2, true);
  51                                 break;
  52                         }
  53                         MC2_yield();
  54                 }
  55 MC2_exitLoop();
  56
  57
  58
  59                 MCID _rmw2 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
  60                 priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
  61         }
  62 MC2_exitLoop();
  63
  64 }
  65
  66 static inline void write_lock(MCID _mrw, rwlock_t *rw)
  67 {
  68         MCID _rmw3 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
  69         int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
  70         MC2_enterLoop();
  71         while(true) {
  72                 MCID _br2;
  73
  74                 int _cond2 = priorvalue != 1048576;
  75                 MCID _cond2_m = MC2_function_id(3, 1, sizeof(_cond2), _cond2, _rmw3);
  76                 if (_cond2) {_br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
  77
  78                         MC2_merge(_br2);
  79                 } else {
  80                         _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);
  81                         break;
  82                 }
  83
  84                 MCID _rmw4 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
  85                 rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
  86
  87                 MC2_enterLoop();
  88                 while (true) {
  89                         MCID _mstatus; _mstatus=MC2_nextOpLoadOffset(_mrw, MC2_OFFSET(rwlock_t *, lock)); int status = load_32(&rw->lock);
  90                         MCID _br3;
  91
  92                         int _cond3 = status != 1048576;
  93                         MCID _cond3_m = MC2_function_id(4, 1, sizeof(_cond3), _cond3, _mstatus);
  94                         if (_cond3) {_br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
  95
  96                                 MC2_merge(_br3);
  97                         } else {
  98                                 _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);
  99                                 break;
 100                         }
 101                         MC2_yield();
 102                 }
 103 MC2_exitLoop();
 104
 105
 106                 MCID _rmw5 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
 107                 priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
 108         }
 109 MC2_exitLoop();
 110
 111 }
 112
 113 static inline bool write_trylock(MCID _mrw, rwlock_t *rw, MCID * retval)
 114 {
 115         MCID _rmw6 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
 116         int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
 117
 118         MCID _fn0; int flag = priorvalue != RW_LOCK_BIAS;
 119         _fn0 = MC2_function_id(7, 1, sizeof (flag), (uint64_t)flag, _rmw6);
 120         MCID _br4;
 121
 122         int _cond4 = !flag;
 123         MCID _cond4_m = MC2_function_id(5, 1, sizeof(_cond4), _cond4, _fn0);
 124         if (_cond4) {
 125                 _br4 = MC2_branchUsesID(_cond4_m, 1, 2, true);
 126                 MCID _rmw7 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
 127                 rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
 128                 MC2_merge(_br4);
 129         }
 130  else { _br4 = MC2_branchUsesID(_cond4_m, 0, 2, true);  MC2_merge(_br4);
 131  }
 132         *retval = _fn0;
 133         return flag;
 134 }
 135
 136 static inline void read_unlock(MCID _mrw, rwlock_t *rw)
 137 {
 138         MCID _rmw8 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
 139         rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
 140 }
 141
 142 static inline void write_unlock(MCID _mrw, rwlock_t *rw)
 143 {
 144         MCID _rmw9 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
 145         rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
 146 }
 147
 148 MCID _fn1; rwlock_t * mylock;
 149 int shareddata;
 150
 151 static void foo() {
 152         MCID _rv0;
 153         int res = write_trylock(MCID_NODEP, mylock, &_rv0);
 154         MCID _br5;
 155
 156         int _cond5 = res;
 157         MCID _cond5_m = MC2_function_id(6, 1, sizeof(_cond5), _cond5, _rv0);
 158         if (_cond5) {
 159                 _br5 = MC2_branchUsesID(_rv0, 1, 2, true);
 160                 write_unlock(MCID_NODEP, mylock);
 161                 MC2_merge(_br5);
 162         } else {_br5 = MC2_branchUsesID(_rv0, 0, 2, true);
 163
 164                 MC2_merge(_br5);
 165         }
 166 }
 167
 168 static void a(void *obj)
 169 {
 170         int i;
 171         MC2_enterLoop();
 172         for(i=0;i<PROBLEMSIZE;i++)
 173                 foo();
 174 MC2_exitLoop();
 175
 176 }
 177
 178 int user_main(int argc, char **argv)
 179 {
 180         mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
 181
 182 _fn1 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock);
 183         thrd_t t1, t2;
 184         //, t3, t4;
 185         MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
 186         store_32(&mylock->lock, RW_LOCK_BIAS);
 187
 188         thrd_create(&t1, (thrd_start_t)&a, NULL);
 189         thrd_create(&t2, (thrd_start_t)&a, NULL);
 190         //      thrd_create(&t3, (thrd_start_t)&a, NULL);
 191         //      thrd_create(&t4, (thrd_start_t)&a, NULL);
 192
 193         thrd_join(t1);
 194         thrd_join(t2);
 195         //      thrd_join(t3);
 196         //      thrd_join(t4);
 197         free(mylock);
 198
 199         return 0;
 200 }