benchmark/seqlock/seqlock.h

   1 #ifndef _SEQLOCK_H
   2 #define _SEQLOCK_H
   3
   4 #include <atomic>
   5
   6 using namespace std;
   7
   8 typedef void* (*read_func_ptr_t)(void*);
   9
  10 /**
  11         Properties to check:
  12         Every read will read the up-to-date value, and only one thread can be
  13         writing.
  14 */
  15
  16
  17 /**
  18         @Begin
  19         @Global_define:
  20                 Type *__data_ptr = NULL;
  21                 bool __is_writing = false;
  22
  23         static bool _is_equals(void* ptr1, void* ptr2) {
  24                 //... Should be defined to check if the internal data equals
  25         }
  26
  27         @Happens-before:
  28                 Init -> Read
  29                 Init -> Write
  30                 Write -> Write
  31                 Write -> Read
  32         @End
  33 */
  34
  35 /**
  36         Fixed the write to be lock-free. Use a CAS in the write instead of using the
  37         mutex. There are a couple options for the implementation according to Hans
  38         Boehm's paper <<Can seqlocks get along with programming language memory
  39         models>>.
  40
  41         Interesting thing in the read() function is the memory ordering we should
  42         impose there. In Hans Boehm's paper, he presents 3 ways to do it. We will
  43         try to use the fences one here as a special case to check programs written
  44         with C++ fences.
  45 */
  46
  47 template<typename Type>
  48 class seqlock {
  49         private:
  50         // To make the write lock-free, we don't need the mutex here.
  51         // Mutex to write exclusively
  52
  53         // Sequence for reader consistency check
  54         atomic_int _seq;
  55         // The shared data structure to be protected;
  56         // It needs to be atomic to avoid data races
  57         atomic<Type*> _data;
  58
  59         // This function is to check if the objects pointed by the two pointer are
  60         // the same; it is only used for checking the correctness
  61         bool is_equal(void *ptr1, void *ptr2) {
  62                 // return ptr1 == NULL ? false : ptr1->equals(ptr2);
  63         }
  64
  65         public:
  66         /**
  67                 @Begin
  68                 @Interface: Init
  69                 @Commit_point_set: Init_Point
  70                 @Action:
  71                         @Code:
  72                         __data_ptr = data;
  73                 @End
  74         */
  75         seqlock(Type *data) {
  76                 _data.store(data, memory_order_relaxed);
  77                 _seq.store(0, memory_order_release);
  78                 /**
  79                         # Initialization code
  80                         @Begin
  81                         @Commit_point_check_define: true
  82                         @Label: Init_Point
  83                         @End
  84                 */
  85         }
  86
  87         ~seqlock() {}
  88
  89         /**
  90                 @Begin
  91                 @Interface: Read
  92                 @Commit_point_set: Read_Success_Point
  93                 @Action:
  94                         @Code:
  95                         void *_Old_data_ptr = __data_ptr;
  96                 @Post_check:
  97                         _is_equal(read_func(_Old_data_ptr), __RET__)
  98                 @End
  99         */
 100         void* read(read_func_ptr_t read_func) {
 101                 while (true) {
 102                         int old_seq = _seq.load(memory_order_acquire);
 103                         if (old_seq % 2 == 1) continue;
 104                         // A customized read of something return a pointer to it
 105                         // Potential data race, should be atomic
 106                         void *res = read_func(_data.load(memory_order_relaxed));
 107                         // This is subtle to use an acquire fence here
 108                         // What we actually need is a #LoadLoad fence
 109                         atomic_thread_fence(memory_order_acquire);
 110                         int new_seq;
 111                         if ((new_seq = _seq.load(memory_order_relaxed)) == old_seq) {
 112                                 /**
 113                                         @Begin
 114                                         @Commit_point_check_define: __ATOMIC_RET__ == old_seq
 115                                         @Label: Read_Success_Point
 116                                         @End
 117                                 */
 118                                 return res;
 119                         }
 120                         // _data has been updated, read should retry
 121                 }
 122         }
 123
 124         /**
 125                 @Begin
 126                 @Interface: Write
 127                 @Commit_point_set: Write_Success_Point
 128                 @Action:
 129                         @Code:
 130                         __data_ptr = new_data;
 131                 @End
 132         */
 133
 134         void write(Type *new_data) {
 135                 while (true) {
 136                         // This might be a relaxed too
 137                         // Should think about how to read the lo
 138                         int old_seq = _seq.load(memory_order_acquire);
 139                         if (old_seq % 2 == 1) {
 140                                 // Backoff, another thread is writing
 141                                 //thrd_yield();
 142                                 continue; // Retry
 143                         }
 144                         // Should be relaxed!!!
 145                         if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
 146                                 memory_order_relaxed, memory_order_relaxed))
 147                                 break;
 148                 }
 149                 // Should be a store release, to synchronize with the fence!!!
 150                 _data.store(new_data, memory_order_release);
 151                 _seq.fetch_add(1, memory_order_release);
 152                 /**
 153                         @Begin
 154                         @Commit_point_define: true
 155                         @Label: Write_Success_Point
 156                         @End
 157                 */
 158         }
 159 };
 160
 161
 162 #endif