test/seqlock2.cc

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