test/seqlock.c

   1 #include <stdio.h>
   2 #include <threads.h>
   3 #include <stdatomic.h>
   4
   5 #include <stdatomic.h>
   6 #include "threads.h"
   7 #include "libinterface.h"
   8
   9 /*atomic_*/ int _seq;
  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, 0);
  17 }
  18
  19 int seqlock_read() {
  20     MC2_enterLoop();
  21     while (true) {
  22         MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
  23
  24         MCID _fn0; int c0 = (old_seq % 2 == 1);
  25         _fn0 = MC2_function(1, sizeof (c0), c0, _mold_seq);
  26         MCID _br0;
  27         if (c0) {
  28             _br0 = MC2_branchUsesID(_fn0, 1, 2, true);
  29             MC2_yield();
  30             MC2_merge(_br0);
  31         } else {
  32             MCID _mres; _br0 = MC2_branchUsesID(_fn0, 0, 2, true);
  33             _mres=MC2_nextOpLoad(MCID_NODEP); int res = load_32(&_data);
  34             MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
  35
  36             MCID _fn1; int c1;
  37             c1 = seq == old_seq;
  38
  39             _fn1 = MC2_function(2, sizeof (c1), c1, _mold_seq, _mseq);              MCID _br1;
  40             if (c1) { // relaxed
  41                 _br1 = MC2_branchUsesID(_fn1, 1, 2, true);
  42                 MC2_exitLoop();
  43                 MCID res_phi = MC2_loop_phi(_mres);
  44                 return res;
  45             } else {
  46                 _br1 = MC2_branchUsesID(_fn1, 0, 2, true);
  47                 MC2_yield();
  48                 MC2_merge(_br1);
  49             }
  50             MC2_merge(_br0);
  51         }
  52     }
  53     MC2_exitLoop();
  54
  55 }
  56
  57 void seqlock_write(MCID _mnew_data, int new_data) {
  58     MC2_enterLoop();
  59     while (true) {
  60         MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
  61         MCID _fn2; int c2 = (old_seq % 2 == 1);
  62         _fn2 = MC2_function(1, sizeof (c2), c2, _mold_seq);
  63         MCID _br2;
  64         if (c2) {
  65             _br2 = MC2_branchUsesID(_fn2, 1, 2, true);
  66             MC2_yield();
  67             MC2_merge(_br2);
  68         } else {
  69             MCID _fn3; _br2 = MC2_branchUsesID(_fn2, 0, 2, true);
  70             int new_seq = old_seq + 1;
  71             _fn3 = MC2_function(1, sizeof (new_seq), new_seq, _mold_seq);
  72             MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn3);
  73             int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
  74             MCID _fn4; int c3 = old_seq == cas_value;
  75             _fn4 = MC2_function(2, sizeof (c3), c3, _mold_seq, _rmw0);
  76             MCID _br3;
  77             if (c3) {
  78                 _br3 = MC2_branchUsesID(_fn4, 1, 2, true);
  79                 break;
  80             } else {
  81                 _br3 = MC2_branchUsesID(_fn4, 0, 2, true);
  82                 MC2_yield();
  83                 MC2_merge(_br3);
  84             }
  85             MC2_merge(_br2);
  86         }
  87     }
  88     MC2_exitLoop();
  89
  90     MC2_nextOpStore(MCID_NODEP, _mnew_data);
  91     store_32(&_data, new_data);
  92
  93     MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
  94     rmw_32(ADD, &_seq, /*dummy */0, 1);
  95 }
  96
  97 static void a(void *obj) {
  98     seqlock_write(MCID_NODEP, 3);
  99 }
 100
 101 static void b(void *obj) {
 102     seqlock_write(MCID_NODEP, 2);
 103 }
 104
 105 static void c(void *obj) {
 106     int r1 = seqlock_read();
 107 }
 108
 109 int user_main(int argc, char **argv) {
 110     thrd_t t1; thrd_t t2; thrd_t t3;
 111     seqlock_init();
 112
 113     thrd_create(&t1, (thrd_start_t)&a, NULL);
 114     thrd_create(&t2, (thrd_start_t)&b, NULL);
 115     thrd_create(&t3, (thrd_start_t)&c, NULL);
 116
 117     thrd_join(t1);
 118     thrd_join(t2);
 119     thrd_join(t3);
 120     return 0;
 121 }