test/seqlock.c

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