test/seqlock2.cc

   1 #include <stdio.h>
   2 #include <threads.h>
   3
   4 #include "libinterface.h"
   5
   6 typedef struct seqlock {
   7         // Sequence for reader consistency check
   8         int _seq;
   9         // It needs to be atomic to avoid data races
  10         int _data;
  11
  12         seqlock() {
  13                 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  14                 store_32(&_seq, 0);
  15                 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  16                 store_32(&_data, 10);
  17         }
  18
  19         int read() {
  20                 int res;
  21                 MC2_enterLoop();
  22                 while (true) {
  23                         //int old_seq = _seq.load(memory_order_acquire); // acquire
  24                         MCID mold_seq = MC2_nextOpLoad(MCID_NODEP);
  25                         int old_seq = load_32(&_seq);
  26
  27                         int cond0 = (old_seq % 2 == 1);
  28                         MCID mcond0 = MC2_function(1, 4, cond0, mold_seq);
  29                         MCID br0;
  30
  31                         if (cond0) {
  32                                 br0 = MC2_branchUsesID(mcond0, 1, 2, true);
  33                                 MC2_yield();
  34                                 MC2_merge(br0);
  35                         } else {
  36                                 br0 = MC2_branchUsesID(mcond0, 0, 2, true);
  37
  38                                 MCID mres = MC2_nextOpLoad(MCID_NODEP);
  39                                 res = load_32(&_data);
  40
  41                                 MCID mseq = MC2_nextOpLoad(MCID_NODEP);
  42                                 int seq = load_32(&_seq); // _seq.load(memory_order_relaxed)
  43
  44                                 int cond1 = seq == old_seq;
  45                                 MCID mcond1 = MC2_function(2, 4, cond1, mseq, mold_seq);
  46                                 MCID br1;
  47                                 if (cond1) { // relaxed
  48                                         br1 = MC2_branchUsesID(mcond1, 1, 2, true);
  49                                         break;
  50                                 } else {
  51                                         br1 = MC2_branchUsesID(mcond1, 0, 2, true);
  52                                         MC2_yield();
  53                                         MC2_merge(br1);
  54                                 }
  55
  56                                 MC2_merge(br0);
  57                         }
  58                 }
  59                 MC2_exitLoop();
  60                 return res;
  61         }
  62
  63         void write(int new_data) {
  64                 MC2_enterLoop();
  65                 while (true) {
  66                         // This might be a relaxed too
  67                         //int old_seq = _seq.load(memory_order_acquire); // acquire
  68                         MCID mold_seq = MC2_nextOpLoad(MCID_NODEP);
  69                         int old_seq = load_32(&_seq);
  70
  71                         int cond0 = (old_seq % 2 == 1);
  72                         MCID mcond0 = MC2_function(1, 4, cond0, mold_seq);
  73                         MCID br0;
  74                         if (cond0) {
  75                                 //retry as the integer is odd
  76                                 br0 = MC2_branchUsesID(mcond0, 1, 2, true);
  77                                 MC2_yield();
  78                                 MC2_merge(br0);
  79                         } else {
  80                                 br0 = MC2_branchUsesID(mcond0, 0, 2, true);
  81
  82                                 int new_seq=old_seq+1;
  83                                 MCID mnew_seq=MC2_function(1, 4, new_seq, mold_seq);
  84                                 MCID m_priorval=MC2_nextRMW(MCID_NODEP, mold_seq, mnew_seq);
  85                                 int cas_value=rmw_32(CAS, &_seq, old_seq, new_seq);
  86                                 int exit=cas_value==old_seq;
  87                                 MCID m_exit=MC2_function(2, 4, exit, m_priorval, mold_seq);
  88
  89                                 if (exit) {
  90                                         MCID br2=MC2_branchUsesID(m_exit, 1, 2, true);
  91                                         break;
  92                                 } else {
  93                                         MCID br2=MC2_branchUsesID(m_exit, 0, 2, true);
  94                                         MC2_yield();
  95                                         MC2_merge(br2);
  96                                 }
  97                                 //if cas fails, we have to retry as someone else succeeded
  98                                 MC2_merge(br0);
  99                         }
 100                 }
 101                 MC2_exitLoop();
 102
 103                 // Update the data
 104                 //_data.store(new_data, memory_order_release); // release
 105                 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
 106                 store_32(&_data, new_data);
 107
 108                 // _seq.fetch_add(1, memory_order_release); // release
 109                 MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
 110                 rmw_32(ADD, &_seq, /* dummy */0, 1);
 111         }
 112
 113 } seqlock_t;
 114
 115
 116 seqlock_t *lock;
 117
 118 static void a(void *obj) {
 119         lock->write(30);
 120 }
 121
 122 static void b(void *obj) {
 123         lock->write(20);
 124 }
 125
 126 static void c(void *obj) {
 127         int r1 = lock->read();
 128 }
 129
 130 int user_main(int argc, char **argv) {
 131         thrd_t t1, t2, t3;
 132         lock = new seqlock_t();
 133
 134         thrd_create(&t1, (thrd_start_t)&a, NULL);
 135         thrd_create(&t2, (thrd_start_t)&b, NULL);
 136         thrd_create(&t3, (thrd_start_t)&c, NULL);
 137
 138         thrd_join(t1);
 139         thrd_join(t2);
 140         thrd_join(t3);
 141         return 0;
 142 }