benchmarks/satcheck/seqlock/seqlock_unannotated.cc

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