benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c

   1 #include <stdlib.h>
   2 #include <stdio.h>
   3 #include <threads.h>
   4 #include <stdbool.h>
   5 #include "libinterface.h"
   6
   7 /** Example implementation of linux rw lock along with 2 thread test
   8  *  driver... */
   9
  10 typedef union {
  11         int lock;
  12 } rwlock_t;
  13
  14 static inline bool write_trylock(MCID _mrw, rwlock_t *rw, MCID * retval)
  15 {
  16         MCID _rmw0 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
  17         int priorvalue=rmw_32(CAS, &rw->lock, 0, 1);
  18         *retval = _rmw0;
  19         return priorvalue;
  20 }
  21
  22 static inline void write_unlock(MCID _mrw, rwlock_t *rw)
  23 {
  24         MC2_nextOpStoreOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
  25         store_32(&rw->lock, 0);
  26 }
  27
  28 MCID _fn0; rwlock_t * mylock;
  29
  30 static void foo() {
  31         MCID _rv0;
  32         int flag=write_trylock(MCID_NODEP, mylock, &_rv0);
  33         MCID _br0;
  34
  35         int _cond0 = flag;
  36         MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _rv0);
  37         if (_cond0) {_br0 = MC2_branchUsesID(_rv0, 1, 2, true);
  38
  39                 MC2_merge(_br0);
  40         } else {
  41                 _br0 = MC2_branchUsesID(_rv0, 0, 2, true);
  42                 write_unlock(MCID_NODEP, mylock);
  43                 MC2_merge(_br0);
  44         }
  45 }
  46
  47 static void a(void *obj)
  48 {
  49         int i;
  50         MC2_enterLoop();
  51         for(i=0;i<PROBLEMSIZE;i++)
  52                 foo();
  53 MC2_exitLoop();
  54
  55 }
  56
  57 int user_main(int argc, char **argv)
  58 {
  59         thrd_t t1, t2;//, t3, t4;
  60         mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
  61         _fn0 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock);
  62         MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
  63         store_32(&mylock->lock, 0);
  64
  65         thrd_create(&t1, (thrd_start_t)&a, NULL);
  66         thrd_create(&t2, (thrd_start_t)&a, NULL);
  67         //thrd_create(&t3, (thrd_start_t)&a, NULL);
  68         //thrd_create(&t4, (thrd_start_t)&a, NULL);
  69
  70         thrd_join(t1);
  71         thrd_join(t2);
  72         //thrd_join(t3);
  73         //thrd_join(t4);
  74
  75
  76
  77         return 0;
  78 }