benchmarks/satcheck-precompiled/dekker/dekker-fences.c

   1 /*
   2  * Dekker's critical section algorithm, implemented with fences.
   3  * Translated to C by Patrick Lam <prof.lam@gmail.com>
   4  *
   5  * URL:
   6  *   http://www.justsoftwaresolutions.co.uk/threading/
   7  */
   8
   9 #include <threads.h>
  10 #include <stdbool.h>
  11 #include "libinterface.h"
  12
  13 /* atomic */ int flag0, flag1;
  14 /* atomic */ int turn;
  15
  16 #define true 1
  17 #define false 0
  18 #define NULL 0
  19
  20 /* uint32_t */ int var = 0;
  21
  22 void p0() {
  23         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  24         store_32(&flag0, true);
  25         // std::atomic_thread_fence(std::memory_order_seq_cst);
  26
  27         MCID _mf1; int f1;
  28         MC2_enterLoop();
  29         while (true)
  30         {
  31                 _mf1=MC2_nextOpLoad(MCID_NODEP), f1 = load_32(&flag1);
  32                 MCID _br0;
  33
  34                 int _cond0 = !f1;
  35                 MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _mf1);
  36                 if (_cond0) {
  37                         _br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
  38                         break;
  39                 }
  40
  41          else { _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);  MC2_merge(_br0);
  42                  }      MCID _br1;
  43                 MCID _m_cond1_m=MC2_nextOpLoad(MCID_NODEP);
  44                 int _cond1 = load_32(&turn);
  45                 MCID _cond1_m = MC2_function_id(2, 1, sizeof(_cond1), _cond1, _m_cond1_m);
  46                 if (_cond1) {
  47                         _br1 = MC2_branchUsesID(_cond1_m, 1, 2, true);
  48                         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  49                         store_32(&flag0, false);
  50                         MC2_enterLoop();
  51                         while(1) {
  52                                 MCID _br2;
  53                                 MCID _m_cond2_m=MC2_nextOpLoad(MCID_NODEP);
  54                                 int _cond2 = !load_32(&turn);
  55                                 MCID _cond2_m = MC2_function_id(3, 1, sizeof(_cond2), _cond2, _m_cond2_m);
  56                                 if (_cond2) {
  57                                         _br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
  58                                         break;
  59                                 }
  60                  else { _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);  MC2_merge(_br2);
  61                                  }
  62                                 MC2_yield();
  63                         }
  64 MC2_exitLoop();
  65
  66
  67                         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  68                         store_32(&flag0, true);
  69                         MC2_merge(_br1);
  70                 } else {
  71                         _br1 = MC2_branchUsesID(_cond1_m, 0, 2, true);
  72                         MC2_yield();
  73                         MC2_merge(_br1);
  74                 }
  75         }
  76 MC2_exitLoop();
  77
  78
  79         // std::atomic_thread_fence(std::memory_order_acquire);
  80
  81         // critical section
  82         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  83         store_32(&var, 1);
  84
  85         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  86         store_32(&turn, 1);
  87         // std::atomic_thread_fence(std::memory_order_release);
  88         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  89         store_32(&flag0, false);
  90 }
  91
  92 void p1() {
  93         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  94         store_32(&flag1, true);
  95         // std::atomic_thread_fence(std::memory_order_seq_cst);
  96
  97         int f0;
  98         MC2_enterLoop();
  99         while (true) {
 100                 MCID _mf0; _mf0=MC2_nextOpLoad(MCID_NODEP); int f0 = load_32(&flag0);
 101                 MCID _br3;
 102
 103                 int _cond3 = !f0;
 104                 MCID _cond3_m = MC2_function_id(4, 1, sizeof(_cond3), _cond3, _mf0);
 105                 if (_cond3) {
 106                         _br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
 107                         break;
 108                 }
 109                  else { _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);  MC2_merge(_br3);
 110                  }
 111                 MCID _br4;
 112                 MCID _m_cond4_m=MC2_nextOpLoad(MCID_NODEP);
 113                 int _cond4 = !load_32(&turn);
 114                 MCID _cond4_m = MC2_function_id(5, 1, sizeof(_cond4), _cond4, _m_cond4_m);
 115                 if (_cond4) {
 116                         _br4 = MC2_branchUsesID(_cond4_m, 1, 2, true);
 117                         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 118                         store_32(&flag1, false);
 119                         MC2_enterLoop();
 120                         while (1) {
 121                                 MCID _br5;
 122                                 MCID _m_cond5_m=MC2_nextOpLoad(MCID_NODEP);
 123                                 int _cond5 = load_32(&turn);
 124                                 MCID _cond5_m = MC2_function_id(6, 1, sizeof(_cond5), _cond5, _m_cond5_m);
 125                                 if (_cond5)
 126                                         {_br5 = MC2_branchUsesID(_cond5_m, 1, 2, true);
 127                                         break;
 128 }        else { _br5 = MC2_branchUsesID(_cond5_m, 0, 2, true);  MC2_merge(_br5);
 129                                  }                      MC2_yield();
 130                         }
 131 MC2_exitLoop();
 132
 133
 134                         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 135                         store_32(&flag1, true);
 136                         // std::atomic_thread_fence(std::memory_order_seq_cst);
 137                         MC2_merge(_br4);
 138                 }
 139  else { _br4 = MC2_branchUsesID(_cond4_m, 0, 2, true);  MC2_merge(_br4);
 140          }      }
 141 MC2_exitLoop();
 142
 143
 144         // std::atomic_thread_fence(std::memory_order_acquire);
 145
 146         // critical section
 147         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 148         store_32(&var, 2);
 149
 150         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 151         store_32(&turn, 0);
 152         // std::atomic_thread_fence(std::memory_order_release);
 153         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 154         store_32(&flag1, false);
 155 }
 156
 157 void p0l(void *a) {
 158         int i;
 159         MC2_enterLoop();
 160         for(i=0;i<PROBLEMSIZE;i++) {
 161                 p0();
 162         }
 163 MC2_exitLoop();
 164
 165 }
 166
 167
 168 void p1l(void *a) {
 169         int i;
 170         MC2_enterLoop();
 171         for(i=0;i<PROBLEMSIZE;i++) {
 172                 p1();
 173         }
 174 MC2_exitLoop();
 175
 176 }
 177
 178
 179 int user_main(int argc, char **argv)
 180 {
 181         thrd_t a, b;
 182
 183         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 184         store_32(&flag0, false);
 185
 186         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 187         store_32(&flag1, false);
 188
 189         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 190         store_32(&turn, 0);
 191
 192         thrd_create(&a, p0l, NULL);
 193         thrd_create(&b, p1l, NULL);
 194
 195         thrd_join(a);
 196         thrd_join(b);
 197
 198         return 0;
 199 }