benchmarks/satcheck-precompiled/seqlock/seqlock.cc

   1 #include <stdio.h>
   2 #include <threads.h>
   3 #include <stdatomic.h>
   4
   5 #include "libinterface.h"
   6
   7 // Sequence for reader consistency check
   8 /*atomic_*/ int _seq;
   9 // It needs to be atomic to avoid data races
  10 /*atomic_*/ int _data;
  11
  12 void seqlock_init() {
  13     MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  14     store_32(&_seq, 0);
  15     MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  16     store_32(&_data, 10);
  17 }
  18
  19 int seqlock_read(MCID * retval) {
  20     MCID _mres; int res;
  21         MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq); // acquire
  22
  23         MCID _br30;
  24
  25         int _cond30 = old_seq % 2 == 1;
  26         MCID _cond30_m = MC2_function_id(31, 1, sizeof(_cond30), _cond30, _mold_seq);
  27         if (_cond30) {
  28         _br30 = MC2_branchUsesID(_cond30_m, 1, 2, true);
  29         res = -1;
  30         MC2_merge(_br30);
  31     } else {
  32                 _br30 = MC2_branchUsesID(_cond30_m, 0, 2, true);
  33                 _mres=MC2_nextOpLoad(MCID_NODEP), res = load_32(&_data);
  34         MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
  35
  36         MCID _br31;
  37
  38         MCID _cond31_m;
  39
  40         int _cond31 = MC2_equals(_mseq, (uint64_t)seq, _mold_seq, (uint64_t)old_seq, &_cond31_m);
  41         if (_cond31) {_br31 = MC2_branchUsesID(_cond31_m, 1, 2, true);
  42
  43                 MC2_merge(_br31);
  44         } else {
  45             _br31 = MC2_branchUsesID(_cond31_m, 0, 2, true);
  46             res = -1;
  47                 MC2_merge(_br31);
  48         }
  49         MC2_merge(_br30);
  50     }
  51     *retval = _mres;
  52     return res;
  53 }
  54
  55 int seqlock_write(MCID _mnew_data, int new_data, MCID * retval) {
  56     MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
  57     int res;
  58
  59     MCID _br32;
  60
  61     int _cond32 = old_seq % 2 == 1;
  62     MCID _cond32_m = MC2_function_id(32, 1, sizeof(_cond32), _cond32, _mold_seq);
  63     if (_cond32) {
  64         _br32 = MC2_branchUsesID(_cond32_m, 1, 2, true);
  65         res = 0;
  66         MC2_merge(_br32);
  67     } else {
  68         MCID _fn0; _br32 = MC2_branchUsesID(_cond32_m, 0, 2, true);
  69         int new_seq = old_seq + 1;
  70         _fn0 = MC2_function_id(33, 1, sizeof (new_seq), (uint64_t)new_seq, _mold_seq);
  71         MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn0);
  72         int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
  73
  74         MCID _br33;
  75
  76         MCID _cond33_m;
  77
  78         int _cond33 = MC2_equals(_rmw0, (uint64_t)cas_value, _mold_seq, (uint64_t)old_seq, &_cond33_m);
  79         if (_cond33) {
  80             // Update the data
  81             _br33 = MC2_branchUsesID(_cond33_m, 1, 2, true);
  82             MC2_nextOpStore(MCID_NODEP, _mnew_data);
  83             store_32(&_data, new_data);
  84                         MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
  85                         rmw_32(ADD, &_seq, /* dummy */0, 1);
  86             res = 1;
  87                 MC2_merge(_br33);
  88         } else {
  89             _br33 = MC2_branchUsesID(_cond33_m, 0, 2, true);
  90             res = 0;
  91                 MC2_merge(_br33);
  92         }
  93         MC2_merge(_br32);
  94     }
  95     *retval = MCID_NODEP;
  96     return res;
  97 }
  98
  99 static void a(void *obj) {
 100         int q;
 101     MC2_enterLoop();
 102     for (int i = 0; i < PROBLEMSIZE; i++) {
 103         MCID _rv0;
 104         q = seqlock_write(MCID_NODEP, 30, &_rv0);
 105         }
 106 MC2_exitLoop();
 107
 108
 109 }
 110
 111 static void b(void *obj) {
 112     int r1;
 113     MC2_enterLoop();
 114     for (int i = 0; i < PROBLEMSIZE; i++) {
 115         MCID _rv1;
 116         r1 = seqlock_read(&_rv1);
 117         }
 118 MC2_exitLoop();
 119
 120
 121 }
 122
 123 static void c(void *obj) {
 124     int r1;
 125     MC2_enterLoop();
 126     for (int i = 0; i < PROBLEMSIZE; i++) {
 127         MCID _rv2;
 128         r1 = seqlock_read(&_rv2);
 129         }
 130 MC2_exitLoop();
 131
 132
 133 }
 134
 135 int user_main(int argc, char **argv) {
 136     thrd_t t1; thrd_t t2; thrd_t t3;
 137     seqlock_init();
 138
 139     thrd_create(&t1, (thrd_start_t)&a, NULL);
 140     thrd_create(&t2, (thrd_start_t)&b, NULL);
 141     thrd_create(&t3, (thrd_start_t)&c, NULL);
 142
 143     thrd_join(t1);
 144     thrd_join(t2);
 145     thrd_join(t3);
 146
 147
 148     return 0;
 149 }