add seqlock
[cdsspec-compiler.git] / benchmark / chase-lev-deque-bugfix / deque.c
1 #include <stdatomic.h>
2 #include <inttypes.h>
3 #include "deque.h"
4 #include <stdlib.h>
5 #include <stdio.h>
6
7 Deque * create() {
8         Deque * q = (Deque *) calloc(1, sizeof(Deque));
9         Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
10         atomic_store_explicit(&q->array, a, memory_order_relaxed);
11         atomic_store_explicit(&q->top, 0, memory_order_relaxed);
12         atomic_store_explicit(&q->bottom, 0, memory_order_relaxed);
13         atomic_store_explicit(&a->size, 2, memory_order_relaxed);
14         return q;
15 }
16
17
18 /**
19         @Begin
20         @Interface_define: Take 
21         @End
22 */
23 int take(Deque *q) {
24         size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
25         /**
26                 @Begin
27                 @Commit_point_define_check: true
28                 @Label: Take_Read_Bottom
29                 @End
30         */
31         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
32         /**
33                 //@Begin
34                 @Commit_point_define_check: true
35                 @Label: Take_Read_Array
36                 @End
37         */
38         atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
39         /**** SPEC (sequential) (testcase1.c) ****/
40         atomic_thread_fence(memory_order_seq_cst);
41         size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
42         /**
43                 //@Begin
44                 @Commit_point_define_check: t != b
45                 @Label: Take_Read_Top
46                 @End
47         */
48         int x;
49         if (t <= b) {
50                 /* Non-empty queue. */
51                 int size = atomic_load_explicit(&a->size,memory_order_relaxed);
52                 x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
53                 /**
54                         //@Begin
55                         @Commit_point_define_check: t != b
56                         @Label: Take_Read_Buffer
57                         @End
58                 */
59                 if (t == b) {
60                         /* Single last element in queue. */
61                         //FIXME: weaken the following seq_cst causes no spec problem
62                         bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
63                                 1, memory_order_seq_cst, memory_order_relaxed);
64                         /**
65                                 //@Begin
66                                 @Commit_point_define_check: succ 
67                                 @Label: Take_CAS_Top
68                                 @End
69                         */
70
71                         /**
72                                 @Begin
73                                 @Additional_ordering_point_define_check: true
74                                 @Label: Take_Additional_Point
75                                 @End
76                         */
77                         if (!succ) {
78                                 /* Failed race. */
79                                 x = EMPTY;
80                         }
81                         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
82                 }
83         } else { /* Empty queue. */
84                 x = EMPTY;
85                 atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
86         }
87         return x;
88 }
89
90 void resize(Deque *q) {
91         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
92         size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
93         size_t new_size=size << 1;
94         Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
95         size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
96         size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
97         atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
98         size_t i;
99         for(i=top; i < bottom; i++) {
100                 atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
101         }
102         /**** detected UL ****/
103         atomic_store_explicit(&q->array, new_a, memory_order_release);
104         //printf("resize\n");
105 }
106
107 /**
108         @Begin
109         @Interface_define: Push
110         @End
111 */
112 void push(Deque *q, int x) {
113         size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
114         /**** SPEC (sequential) ****/
115         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
116         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
117         if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
118                 resize(q);
119                 // CDSSpec can actually detect the same bug if we avoid the UL error
120                 //Bug in paper...should have next line...
121                 //a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
122                 /**
123                         //@Begin
124                         @Commit_point_define_check: true
125                         @Label: Push_Read_Array
126                         @End
127                 */
128         }
129         int size = atomic_load_explicit(&a->size, memory_order_relaxed);
130
131         atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
132         /**
133                 //@Begin
134                 @Commit_point_define_check: true
135                 @Label: Push_Update_Buffer
136                 @End
137         */
138         /**** SPEC (Sync) (run with -u100 to avoid the uninitialized bug) ****/
139         atomic_thread_fence(memory_order_release);
140         // Watch out!!! We need to specifiy the fence as the commit point because
141         // the synchronization in C11 actually is established at the fence.
142         /**
143                 @Begin
144                 @Commit_point_define_check: true
145                 @Label: Push_Update_Bottom
146                 @End
147         */
148         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
149         
150 }
151
152 /**
153         @Begin
154         @Interface_define: Steal 
155         @End
156 */
157 int steal(Deque *q) {
158         //Watch out: actually on need to be an acquire (don't count it)
159         // An old bug
160         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
161         /**
162                 //@Begin
163                 @Potential_commit_point_define: true
164                 @Label: Steal_Potential_Read_Tail
165                 @End
166         */
167         //FIXME: remove the fence causes no error and fewer executions..
168         atomic_thread_fence(memory_order_seq_cst);
169         /**** SPEC & UL ****/
170         size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
171         /**
172                 @Begin
173                 @Commit_point_define_check: true 
174                 @Label: Steal_Read_Bottom
175                 @End
176         */
177
178         /**
179                 //@Begin
180                 @Commit_point_define: t >= b
181                 @Potential_commit_point_label: Steal_Potential_Read_Tail
182                 @Label: Steal_Read_Tail
183                 @End
184         */
185         int x = EMPTY;
186         if (t < b) {
187                 /* Non-empty queue. */
188                 /**** detected UL ****/
189                 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
190                 /**
191                         //@Begin
192                         @Commit_point_define_check: true
193                         @Label: Steal_Read_Array
194                         @End
195                 */
196                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
197                 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
198                 /**
199                         //@Begin
200                         @Potential_commit_point_define: true
201                         @Label: Steal_Potential_Read_Buffer
202                         @End
203                 */
204                 /**** SPEC (sequential) ****/ 
205                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
206                         memory_order_seq_cst, memory_order_relaxed);
207                 /**
208                         //@Begin
209                         @Commit_point_define_check: succ
210                         @Label: Steal_CAS_Top
211                         @End
212                 */
213
214                 /**
215                         @Begin
216                         @Additional_ordering_point_define_check: true 
217                         @Label: Steal_Additional_Point
218                         @End
219                 */
220
221                 /**
222                         //@Begin
223                         @Commit_point_define: succ
224                         @Potential_commit_point_label: Steal_Potential_Read_Buffer
225                         @Label: Steal_Read_Buffer
226                         @End
227                 */
228                 if (!succ) {
229                         /* Failed race. */
230                         return ABORT;
231                 }
232         }
233         return x;
234 }