benchmarks/satcheck-precompiled/seqlock/seqlock_unannotated.cc

   1 #include <stdio.h>
   2 #include <threads.h>
   3
   4 #include "libinterface.h"
   5
   6 // Sequence for reader consistency check
   7 /*atomic_*/ int _seq;
   8 // It needs to be atomic to avoid data races
   9 /*atomic_*/ int _data;
  10
  11 void seqlock_init() {
  12     store_32(&_seq, 0);
  13     store_32(&_data, 10);
  14 }
  15
  16 int seqlock_read() {
  17     int res;
  18         int old_seq = load_32(&_seq); // acquire
  19
  20         if (old_seq % 2 == 1) {
  21         res = -1;
  22     } else {
  23                 res = load_32(&_data);
  24         int seq = load_32(&_seq);
  25
  26         if (seq == old_seq) {
  27         } else {
  28             res = -1;
  29         }
  30     }
  31     return res;
  32 }
  33
  34 int seqlock_write(int new_data) {
  35     int old_seq = load_32(&_seq);
  36     int res;
  37
  38     if (old_seq % 2 == 1) {
  39         res = 0;
  40     } else {
  41         int new_seq = old_seq + 1;
  42         int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
  43
  44         if (cas_value == old_seq) {
  45             // Update the data
  46             store_32(&_data, new_data);
  47                         rmw_32(ADD, &_seq, /* dummy */0, 1);
  48             res = 1;
  49         } else {
  50             res = 0;
  51         }
  52     }
  53     return res;
  54 }
  55
  56 static void a(void *obj) {
  57         int q;
  58     for (int i = 0; i < PROBLEMSIZE; i++) {
  59         q = seqlock_write(30);
  60         }
  61
  62 }
  63
  64 static void b(void *obj) {
  65     int r1;
  66     for (int i = 0; i < PROBLEMSIZE; i++) {
  67         r1 = seqlock_read();
  68         }
  69
  70 }
  71
  72 static void c(void *obj) {
  73     int r1;
  74     for (int i = 0; i < PROBLEMSIZE; i++) {
  75         r1 = seqlock_read();
  76         }
  77
  78 }
  79
  80 int user_main(int argc, char **argv) {
  81     thrd_t t1; thrd_t t2; thrd_t t3;
  82     seqlock_init();
  83
  84     thrd_create(&t1, (thrd_start_t)&a, NULL);
  85     thrd_create(&t2, (thrd_start_t)&b, NULL);
  86     thrd_create(&t3, (thrd_start_t)&c, NULL);
  87
  88     thrd_join(t1);
  89     thrd_join(t2);
  90     thrd_join(t3);
  91
  92
  93     return 0;
  94 }