benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c

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