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