clang/test/seqlock.c

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