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  else { _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);  MC2_merge(_br0);
  41  }
  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);
 140                         MC2_yield();
 141          MC2_merge(_br4);
 142          }      }
 143 MC2_exitLoop();
 144
 145
 146         // std::atomic_thread_fence(std::memory_order_acquire);
 147
 148         // critical section
 149         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 150         store_32(&var, 2);
 151
 152         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 153         store_32(&turn, 0);
 154         // std::atomic_thread_fence(std::memory_order_release);
 155         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 156         store_32(&flag1, false);
 157 }
 158
 159 void p0l(void *a) {
 160         int i;
 161         MC2_enterLoop();
 162         for(i=0;i<PROBLEMSIZE;i++) {
 163                 p0();
 164         }
 165 MC2_exitLoop();
 166
 167 }
 168
 169
 170 void p1l(void *a) {
 171         int i;
 172         MC2_enterLoop();
 173         for(i=0;i<PROBLEMSIZE;i++) {
 174                 p1();
 175         }
 176 MC2_exitLoop();
 177
 178 }
 179
 180
 181 int user_main(int argc, char **argv)
 182 {
 183         thrd_t a, b;
 184
 185         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 186         store_32(&flag0, false);
 187
 188         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 189         store_32(&flag1, false);
 190
 191         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 192         store_32(&turn, 0);
 193
 194         thrd_create(&a, p0l, NULL);
 195         thrd_create(&b, p1l, NULL);
 196
 197         thrd_join(a);
 198         thrd_join(b);
 199
 200         return 0;
 201 }