more data structures
[cdsspec-compiler.git] / 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