benchmarks/satcheck-precompiled/seqlock/seqlock.cc

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