save
[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         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
26         atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
27         atomic_thread_fence(memory_order_seq_cst);
28         size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
29         /**
30                 @Begin
31                 @Commit_point_define_check: t > b
32                 @Label: Take_Point_1
33                 @End
34         */
35         int x;
36         if (t <= b) {
37                 /* Non-empty queue. */
38                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
39                 if (size == 0) 
40                         model_print("take: size == 0\n");
41                 // TODO: size can be zero here!!
42                 x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
43                 /**
44                         @Begin
45                         @Commit_point_define_check: t != b
46                         @Label: Take_Point2
47                         @End
48                 */
49                 if (t == b) {
50                         /* Single last element in queue. */
51                         bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
52                                 1, memory_order_seq_cst, memory_order_relaxed);
53                         /**
54                                 @Begin
55                                 @Commit_point_define_check: succ == true
56                                 @Label: Take_Point3
57                                 @End
58                         */
59                         
60                         /**
61                                 @Begin
62                                 @Commit_point_define_check: succ == false
63                                 @Label: Take_Point4
64                                 @End
65                         */
66                         if (!succ) {
67                                 /* Failed race. */
68                                 x = EMPTY;
69                         }
70                         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
71                 }
72         } else { /* Empty queue. */
73                 x = EMPTY;
74                 atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
75         }
76         return x;
77 }
78
79 void resize(Deque *q) {
80         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
81         size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
82         size_t new_size=size << 1;
83         Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
84         size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
85         size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
86         atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
87         size_t i;
88         for(i=top; i < bottom; i++) {
89                 if (new_size == 0)
90                         model_print("resize: new_size == 0\n");
91                 if (size == 0)
92                         model_print("resize: size == 0\n");
93                 atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
94         }
95         atomic_store_explicit(&q->array, new_a, memory_order_release);
96         printf("resize\n");
97 }
98
99 /**
100         @Begin
101         @Interface_define: Push
102         @End
103 */
104 void push(Deque *q, int x) {
105         size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
106         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
107         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
108         if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
109                 resize(q);
110                 //Bug in paper...should have next line...
111                 a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
112         }
113         int size = atomic_load_explicit(&a->size, memory_order_relaxed);
114         if (size == 0) 
115                 model_print("push: size == 0\n");
116         atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
117         atomic_thread_fence(memory_order_release);
118         /**
119                 @Begin
120                 @Commit_point_define_check: true
121                 @Label: Push_Point
122                 @End
123         */
124         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
125 }
126
127 /**
128         @Begin
129         @Interface_define: Steal 
130         @End
131 */
132 int steal(Deque *q) {
133         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
134         atomic_thread_fence(memory_order_seq_cst);
135         size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
136         /**
137                 @Begin
138                 @Commit_point_define_check: t >= b
139                 @Label: Steal_Point1
140                 @End
141         */
142         int x = EMPTY;
143         if (t < b) {
144                 /* Non-empty queue. */
145                 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
146                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
147                 if (size == 0) 
148                         model_print("steal: size == 0\n");
149                 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
150                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
151                         memory_order_seq_cst, memory_order_relaxed);
152                 /**
153                         @Begin
154                         @Commit_point_define_check: succ == true
155                         @Label: Steal_Point2
156                         @End
157                 */
158                 
159                 /**
160                         @Begin
161                         @Commit_point_define_check: succ == false
162                         @Label: Steal_Point3
163                         @End
164                 */
165                 if (!succ) {
166                         /* Failed race. */
167                         return ABORT;
168                 }
169         }
170         return x;
171 }