clang/test/seqlock.c

   1 #include <stdio.h>
   2
   3 #include "threads.h"
   4 #include "libinterface.h"
   5 #define PROBLEMSIZE 100
   6
   7 /*atomic_*/ int _seq;
   8 /*atomic_*/ int _data;
   9
  10 void seqlock_init() {
  11     MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  12     store_32(&_seq, 0);
  13     MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  14     store_32(&_data, 10);
  15 }
  16
  17 int seqlock_read(MCID * retval) {
  18     MCID _mres; int res;
  19     MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
  20
  21     MCID _br0;
  22
  23     int _cond0 = old_seq % 2 == 1;
  24     MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _mold_seq);
  25     if (_cond0) {
  26         _br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
  27         res = -1;
  28         MC2_merge(_br0);
  29     } else {
  30         _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);
  31         _mres=MC2_nextOpLoad(MCID_NODEP), res = load_32(&_data);
  32         MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
  33
  34         MCID _br1;
  35
  36         MCID _cond1_m;
  37
  38         int _cond1 = MC2_equals(_mseq, seq, _mold_seq, old_seq, &_cond1_m);
  39         if (_cond1) {_br1 = MC2_branchUsesID(_cond1_m, 1, 2, true);
  40              // relaxed
  41             MC2_merge(_br1);
  42         } else {
  43             _br1 = MC2_branchUsesID(_cond1_m, 0, 2, true);
  44             res = -1;
  45             MC2_merge(_br1);
  46         }
  47         MC2_merge(_br0);
  48     }
  49     *retval = _mres;
  50     return res;
  51 }
  52
  53 int seqlock_write(MCID _mnew_data, int new_data, MCID * retval) {
  54     MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
  55     int res;
  56     MCID _br2;
  57
  58     int _cond2 = old_seq % 2 == 1;
  59     MCID _cond2_m = MC2_function_id(2, 1, sizeof(_cond2), _cond2, _mold_seq);
  60     if (_cond2) {
  61         _br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
  62         res = 0;
  63         MC2_merge(_br2);
  64     } else {
  65         MCID _fn0; _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);
  66         int new_seq = old_seq + 1;
  67         _fn0 = MC2_function_id(3, 1, sizeof (new_seq), new_seq, _mold_seq);
  68         MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn0);
  69         int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
  70         MCID _br3;
  71
  72         MCID _cond3_m;
  73
  74         int _cond3 = MC2_equals(_rmw0, cas_value, _mold_seq, old_seq, &_cond3_m);
  75         if (_cond3) {
  76             _br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
  77             MC2_nextOpStore(MCID_NODEP, _mnew_data);
  78             store_32(&_data, new_data);
  79             MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
  80             rmw_32(ADD, &_seq, /*dummy */0, 1);
  81             res = 1;
  82             MC2_merge(_br3);
  83         } else {
  84             _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);
  85             res = 0;
  86             MC2_merge(_br3);
  87         }
  88         MC2_merge(_br2);
  89     }
  90     *retval = MCID_NODEP;
  91     return res;
  92 }
  93
  94 static void a(void *obj) {
  95     MC2_enterLoop();
  96     for (int i = 0; i < PROBLEMSIZE; i++)
  97         seqlock_write(30);
  98 MC2_exitLoop();
  99
 100 }
 101
 102 static void b(void *obj) {
 103     int r1;
 104     MC2_enterLoop();
 105     for (int i = 0; i < PROBLEMSIZE; i++)
 106         MCID _rv0;
 107         r1 = seqlock_read(&_rv0);
 108 MC2_exitLoop();
 109
 110 }
 111
 112 static void c(void *obj) {
 113     int r1;
 114     MC2_enterLoop();
 115     for (int i = 0; i < PROBLEMSIZE; i++)
 116         MCID _rv1;
 117         r1 = seqlock_read(&_rv1);
 118 MC2_exitLoop();
 119
 120 }
 121
 122 int user_main(int argc, char **argv) {
 123     thrd_t t1; thrd_t t2; thrd_t t3;
 124     seqlock_init();
 125
 126     thrd_create(&t1, (thrd_start_t)&a, NULL);
 127     thrd_create(&t2, (thrd_start_t)&b, NULL);
 128     thrd_create(&t3, (thrd_start_t)&c, NULL);
 129
 130     thrd_join(t1);
 131     thrd_join(t2);
 132     thrd_join(t3);
 133     return 0;
 134 }