benchmark/seqlock/seqlock.h

   1 #ifndef _SEQLOCK_H
   2 #define _SEQLOCK_H
   3
   4 #include <stdatomic.h>
   5 #include <unrelacy.h>
   6
   7 #include <spec_lib.h>
   8 #include <stdlib.h>
   9 #include <cdsannotate.h>
  10 #include <specannotation.h>
  11 #include <model_memory.h>
  12 #include "common.h"
  13
  14 using namespace std;
  15
  16 typedef void* (*read_func_ptr_t)(void*);
  17
  18 /**
  19         Properties to check:
  20         Every read will read the up-to-date value, and only one thread can be
  21         writing.
  22 */
  23
  24 /**
  25         Fixed the write to be lock-free. Use a CAS in the write instead of using the
  26         mutex. There are a couple options for the implementation according to Hans
  27         Boehm's paper <<Can seqlocks get along with programming language memory
  28         models>>.
  29
  30         Interesting thing in the read() function is the memory ordering we should
  31         impose there. In Hans Boehm's paper, he presents 3 ways to do it. We will
  32         try to use the fences one here as a special case to check programs written
  33         with C++ fences.
  34 */
  35
  36 typedef struct Data {
  37         int data1, data2;
  38 } Data;
  39
  40 bool equal(int64_t p1, int64_t p2) {
  41         if (!p1 || !p2)
  42                 return false;
  43         Data *d1 = (Data*) p1;
  44         Data *d2 = (Data*) p2;
  45         if (d1->data1 == d2->data1 &&
  46                 d1->data2 == d2->data2) {
  47                 return true;
  48         } else {
  49                 return false;
  50         }
  51 }
  52
  53
  54 /**
  55     @Begin
  56         @Class_begin
  57         @End
  58 */
  59 class seqlock {
  60         private:
  61         // Sequence for reader consistency check
  62         atomic_int _seq;
  63
  64         // The shared data structure to be protected;
  65         // It needs to be atomic to avoid data races
  66         atomic_int _data1;
  67         atomic_int _data2;
  68
  69         /**
  70                 @Begin
  71                 @Options:
  72                         LANG = CPP;
  73                         CLASS = seqlock;
  74                 @Global_define:
  75                         @DeclareVar:
  76                                 IntegerList *set;
  77                         @InitVar:
  78                                 set = createIntegerList();
  79                                 Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
  80                                 d->data1 = 0;
  81                                 d->data2 = 0;
  82                                 push_back(set, (int64_t) d);
  83                         @Finalize:
  84                                 if (set)
  85                                         destroyIntegerList(set);
  86                                 return true;
  87                 @DefineFunc:
  88                         // This is a trick to get unique id
  89                         // The testcase should have a unique sum
  90                         call_id_t getID(int64_t d1, int64_t d2) {
  91                                 return d1 + d2;
  92                         }
  93                         @DefineFunc:
  94                         bool print(int64_t p) {
  95                                 Data *d = (Data*) p;
  96                                 model_print("Elem-> d1 = %d, d2 = %d\n", d->data1, d->data2);
  97                         }
  98                 @DefineFunc:
  99                         void _write(int64_t d1, int64_t d2) {
 100                                 Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
 101                                 d->data1 = d1;
 102                                 d->data2 = d2;
 103                                 push_back(set, (int64_t) d);
 104                         }
 105                 @DefineFunc:
 106                         bool _read(int d1, int d2) {
 107                                 Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
 108                                 d->data1 = d1;
 109                                 d->data2 = d2;
 110                                 bool hasElem = has_elem_by_value(set, (int64_t) d, &equal);
 111                                 return hasElem;
 112                         }
 113                 @Happens_before:
 114                         Write -> Write
 115                         Write -> Read
 116                 @Commutativity: Write <-> Read: true
 117                 @End
 118         */
 119
 120         public:
 121         seqlock() {
 122                 _data1.store(0, memory_order_relaxed);
 123                 _data2.store(0, memory_order_relaxed);
 124                 _seq.store(0, memory_order_relaxed);
 125
 126                 /**
 127                     @Begin
 128                         @Entry_point
 129                         @End
 130                 */
 131         }
 132
 133         ~seqlock() {}
 134
 135         /**
 136                 @Begin
 137                 @Interface: Read
 138                 @Commit_point_set: ReadPoint
 139                 @ID: getID(*d1, *d2)
 140                 //@Action:
 141                         //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(*d1, *d2),
 142                         //      *d1, *d2);
 143                         //do_by_value(set, &print);
 144                 @Post_check:
 145                         _read(*d1, *d2);
 146                 @End
 147         */
 148         void read(int *d1, int *d2) {
 149                 while (true) {
 150                         /**** SPEC (sequential) ****/
 151                         int seq1 = _seq.load(memory_order_acquire);
 152                         printf("seq1=%d\n", seq1);
 153                         if (seq1 & 0x1 == 1) {
 154                                 thrd_yield();
 155                                 continue;
 156                         }
 157                         // Try to read the data
 158                         *d1 = _data1.load(memory_order_relaxed);
 159                         *d2 = _data2.load(memory_order_relaxed);
 160                         /**** SPEC (sequential) ****/
 161                         atomic_thread_fence(memory_order_acquire);
 162
 163                         printf("d1=%d\n", *d1);
 164                         printf("d2=%d\n", *d2);
 165                         // Now doulbe check nothing got updated
 166                         int seq2 = _seq.load(memory_order_relaxed);
 167                         /**
 168                                 @Begin
 169                                 @Commit_point_define_check: seq1 == seq2
 170                                 @Label: ReadPoint
 171                                 @End
 172                         */
 173                         printf("seq2=%d\n", seq1);
 174                         if (seq1 == seq2) { // Good to go
 175                                 printf("Result: d1=%d, d2=%d\n", *d1, *d2);
 176                                 return;
 177                         } else {
 178                                 thrd_yield();
 179                         }
 180                 }
 181         }
 182
 183         /**
 184                 @Begin
 185                 @Interface: Write
 186                 @Commit_point_set: WritePoint
 187                 @ID: getID(d1, d2);
 188                 @Action:
 189                         //model_print("Write_ID = %d, d1=%d, d2=%d\n", getID(d1, d2), d1, d2);
 190                         _write(d1, d2);
 191                         //do_by_value(set, &print);
 192                 @End
 193         */
 194         void write(int d1, int d2) {
 195                 int seq;
 196                 while (true) {
 197                         /**** admissibility ****/
 198                         seq = _seq.load(memory_order_acquire);
 199                         if (seq & 0x1) {
 200                                 thrd_yield();
 201                                 continue;
 202                         }
 203                         bool succ = _seq.compare_exchange_strong(seq, seq + 1,
 204                                 memory_order_relaxed, memory_order_relaxed);
 205                         if (succ) {
 206                                 break;
 207                         } else {
 208                                 thrd_yield();
 209                         }
 210                 }
 211                 /**** SPEC (sequential) ****/
 212                 atomic_thread_fence(memory_order_release);
 213                 _data1.store(d1, memory_order_relaxed);
 214                 _data2.store(d2, memory_order_relaxed);
 215                 // Should be a store release!!!
 216                 /**** admissibility ****/
 217                 _seq.fetch_add(1, memory_order_release);
 218                 /**
 219                         @Begin
 220                         @Commit_point_define_check: true
 221                         @Label: WritePoint
 222                         @End
 223                 */
 224         }
 225 };
 226 /**
 227     @Begin
 228         @Class_end
 229         @End
 230 */
 231
 232
 233 #endif