benchmarks/nidhugg/dekker/dekker-fences.cc.in

   1 /*
   2  * Dekker's critical section algorithm, implemented with fences.
   3  *
   4  * URL:
   5  *   http://www.justsoftwaresolutions.co.uk/threading/
   6  */
   7
   8 #include <atomic>
   9 #include <pthread.h>
  10
  11 std::atomic<bool> flag0, flag1;
  12 std::atomic<int> turn;
  13 std::atomic<int> var;
  14
  15 extern "C" {
  16 void __VERIFIER_assume(int b);
  17 }
  18
  19 void p0() {
  20         flag0.store(true, std::memory_order_relaxed);
  21
  22         while (flag1.load()) {
  23                 if (turn.load() !=0)
  24                 {
  25                         flag0.store(false, std::memory_order_relaxed);
  26                         while (turn.load() != 0) {
  27                                 __VERIFIER_assume(0);
  28                                 //pthread_yield();
  29                         }
  30                         flag0.store(true, std::memory_order_relaxed);
  31                 } else
  32                                 __VERIFIER_assume(0);
  33                         ;
  34                 //                      pthread_yield();
  35         }
  36
  37         // critical section
  38         var.store(1, std::memory_order_relaxed);
  39
  40         turn.store(1, std::memory_order_relaxed);
  41         flag0.store(false, std::memory_order_relaxed);
  42 }
  43
  44 void p1() {
  45         flag1.store(true, std::memory_order_relaxed);
  46
  47         while (flag0.load()) {
  48                 if (turn.load() != 1) {
  49                         flag1.store(false, std::memory_order_relaxed);
  50                         while (turn.load() != 1) {
  51                                 __VERIFIER_assume(0);
  52                                 //pthread_yield();
  53                         }
  54                         flag1.store(true, std::memory_order_relaxed);
  55                 } else
  56                         __VERIFIER_assume(0);
  57                         ;//pthread_yield();
  58         }
  59
  60         // critical section
  61         var.store(2, std::memory_order_relaxed);
  62
  63         turn.store(0, std::memory_order_relaxed);
  64         flag1.store(false, std::memory_order_relaxed);
  65 }
  66
  67 void * p0l(void *arg) {
  68 problemsize             p0();
  69         return NULL;
  70 }
  71
  72 void * p1l(void *arg) {
  73 problemsize             p1();
  74         return NULL;
  75 }
  76
  77 int main(int argc, char **argv)
  78 {
  79         pthread_t a, b;
  80
  81         flag0 = false;
  82         flag1 = false;
  83         turn = 0;
  84         var=0;
  85
  86         pthread_create(&a, 0, p0l, NULL);
  87         pthread_create(&b, 0, p1l, NULL);
  88
  89         pthread_join(a, 0);
  90         pthread_join(b, 0);
  91
  92         return 0;
  93 }