17bd003bbed685859cd36e3839338068eade5678
[c11tester.git] / cmodelint.cc
1 #include <stdio.h>
2 #include "model.h"
3 #include "action.h"
4 #include "cmodelint.h"
5 #include "threads-model.h"
6
7 memory_order orders[6] = {
8         memory_order_relaxed, memory_order_consume, memory_order_acquire,
9         memory_order_release, memory_order_acq_rel, memory_order_seq_cst
10 };
11
12 /** Performs a read action.*/
13 uint64_t model_read_action(void * obj, memory_order ord) {
14         return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
15 }
16
17 /** Performs a write action.*/
18 void model_write_action(void * obj, memory_order ord, uint64_t val) {
19         model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val));
20 }
21
22 /** Performs an init action. */
23 void model_init_action(void * obj, uint64_t val) {
24         model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
25 }
26
27 /**
28  * Performs the read part of a RMW action. The next action must either be the
29  * write part of the RMW action or an explicit close out of the RMW action w/o
30  * a write.
31  */
32 uint64_t model_rmwr_action(void *obj, memory_order ord) {
33         return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
34 }
35
36 /**
37  * Performs the read part of a RMW CAS action. The next action must
38  * either be the write part of the RMW action or an explicit close out
39  * of the RMW action w/o a write.
40  */
41 uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) {
42        return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size));
43 }
44
45
46 /** Performs the write part of a RMW action. */
47 void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
48         model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
49 }
50
51 /** Closes out a RMW action without doing a write. */
52 void model_rmwc_action(void *obj, memory_order ord) {
53         model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
54 }
55
56 /** Issues a fence operation. */
57 void model_fence_action(memory_order ord) {
58         model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
59 }
60
61 /* ---  helper functions --- */
62 uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, const char *position) {
63         return model->switch_to_master(
64                 new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj)
65         );
66 }
67
68 uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
69         return model->switch_to_master(
70                 new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)
71         );
72 }
73
74 void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) {
75         model->switch_to_master(
76                 new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)
77         );
78 }
79
80 void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) {
81         model->switch_to_master(
82                 new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)
83         );
84 }
85
86 // cds atomic inits
87 void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
88         model->switch_to_master(
89                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
90         );
91 }
92 void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
93         model->switch_to_master(
94                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
95         );
96 }
97 void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
98         model->switch_to_master(
99                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
100         );
101 }
102 void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
103         model->switch_to_master(
104                 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
105         );
106 }
107
108
109 // cds atomic loads
110 uint8_t cds_atomic_load8(void * obj, int atomic_index, const char * position) { 
111         return (uint8_t) ( model->switch_to_master(
112                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
113         );
114 }
115 uint16_t cds_atomic_load16(void * obj, int atomic_index, const char * position) {
116         return (uint16_t) ( model->switch_to_master(
117                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
118         );
119 }
120 uint32_t cds_atomic_load32(void * obj, int atomic_index, const char * position) {
121         return (uint32_t) ( model->switch_to_master(
122                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
123         );
124 }
125 uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) {
126         return model->switch_to_master(
127                 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)
128         );
129 }
130
131 // cds atomic stores
132 void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
133         model->switch_to_master(
134                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
135         );
136 }
137 void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
138         model->switch_to_master(
139                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
140         );
141 }
142 void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
143         model->switch_to_master(
144                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
145         );
146 }
147 void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
148         model->switch_to_master(
149                 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
150         );
151 }
152
153 #define _ATOMIC_RMW_(__op__, size, addr, val, atomic_index, position)            \
154 ({                                                                      \
155   uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index, position);   \
156   uint##size##_t _copy = _old;                                          \
157   uint##size##_t _val = val;                                            \
158   _copy __op__ _val;                                                    \
159   model_rmw_action_helper(addr, (uint64_t) _copy, atomic_index, position);        \
160   return _old;                                                          \
161 })
162
163 // cds atomic exchange
164 uint8_t cds_atomic_exchange8(void* addr, uint8_t val, int atomic_index, const char * position) {
165         _ATOMIC_RMW_( = , 8, addr, val, atomic_index, position);
166 }
167 uint16_t cds_atomic_exchange16(void* addr, uint16_t val, int atomic_index, const char * position) {
168         _ATOMIC_RMW_( = , 16, addr, val, atomic_index, position);
169 }
170 uint32_t cds_atomic_exchange32(void* addr, uint32_t val, int atomic_index, const char * position) {
171         _ATOMIC_RMW_( = , 32, addr, val, atomic_index, position);
172 }
173 uint64_t cds_atomic_exchange64(void* addr, uint64_t val, int atomic_index, const char * position) {
174         _ATOMIC_RMW_( = , 64, addr, val, atomic_index, position);
175 }
176
177 // cds atomic fetch add
178 uint8_t cds_atomic_fetch_add8(void* addr, uint8_t val, int atomic_index, const char * position) {
179         _ATOMIC_RMW_( += , 8, addr, val, atomic_index, position);
180 }
181 uint16_t cds_atomic_fetch_add16(void* addr, uint16_t val, int atomic_index, const char * position) {
182         _ATOMIC_RMW_( += , 16, addr, val, atomic_index, position);
183 }
184 uint32_t cds_atomic_fetch_add32(void* addr, uint32_t val, int atomic_index, const char * position) {
185         _ATOMIC_RMW_( += , 32, addr, val, atomic_index, position);
186 }
187 uint64_t cds_atomic_fetch_add64(void* addr, uint64_t val, int atomic_index, const char * position) {
188         _ATOMIC_RMW_( += , 64, addr, val, atomic_index, position);
189 }
190
191 // cds atomic fetch sub
192 uint8_t cds_atomic_fetch_sub8(void* addr, uint8_t val, int atomic_index, const char * position) {
193         _ATOMIC_RMW_( -= , 8, addr, val, atomic_index, position);
194 }
195 uint16_t cds_atomic_fetch_sub16(void* addr, uint16_t val, int atomic_index, const char * position) {
196         _ATOMIC_RMW_( -= , 16, addr, val, atomic_index, position);
197 }
198 uint32_t cds_atomic_fetch_sub32(void* addr, uint32_t val, int atomic_index, const char * position) {
199         _ATOMIC_RMW_( -= , 32, addr, val, atomic_index, position);
200 }
201 uint64_t cds_atomic_fetch_sub64(void* addr, uint64_t val, int atomic_index, const char * position) {
202         _ATOMIC_RMW_( -= , 64, addr, val, atomic_index, position);
203 }
204
205 // cds atomic fetch and
206 uint8_t cds_atomic_fetch_and8(void* addr, uint8_t val, int atomic_index, const char * position) {
207         _ATOMIC_RMW_( &= , 8, addr, val, atomic_index, position);
208 }
209 uint16_t cds_atomic_fetch_and16(void* addr, uint16_t val, int atomic_index, const char * position) {
210         _ATOMIC_RMW_( &= , 16, addr, val, atomic_index, position);
211 }
212 uint32_t cds_atomic_fetch_and32(void* addr, uint32_t val, int atomic_index, const char * position) {
213         _ATOMIC_RMW_( &= , 32, addr, val, atomic_index, position);
214 }
215 uint64_t cds_atomic_fetch_and64(void* addr, uint64_t val, int atomic_index, const char * position) {
216         _ATOMIC_RMW_( &= , 64, addr, val, atomic_index, position);
217 }
218
219 // cds atomic fetch or
220 uint8_t cds_atomic_fetch_or8(void* addr, uint8_t val, int atomic_index, const char * position) {
221         _ATOMIC_RMW_( |= , 8, addr, val, atomic_index, position);
222 }
223 uint16_t cds_atomic_fetch_or16(void* addr, uint16_t val, int atomic_index, const char * position) {
224         _ATOMIC_RMW_( |= , 16, addr, val, atomic_index, position);
225 }
226 uint32_t cds_atomic_fetch_or32(void* addr, uint32_t val, int atomic_index, const char * position) {
227         _ATOMIC_RMW_( |= , 32, addr, val, atomic_index, position);
228 }
229 uint64_t cds_atomic_fetch_or64(void* addr, uint64_t val, int atomic_index, const char * position) {
230         _ATOMIC_RMW_( |= , 64, addr, val, atomic_index, position);
231 }
232
233 // cds atomic fetch xor
234 uint8_t cds_atomic_fetch_xor8(void* addr, uint8_t val, int atomic_index, const char * position) {
235         _ATOMIC_RMW_( ^= , 8, addr, val, atomic_index, position);
236 }
237 uint16_t cds_atomic_fetch_xor16(void* addr, uint16_t val, int atomic_index, const char * position) {
238         _ATOMIC_RMW_( ^= , 16, addr, val, atomic_index, position);
239 }
240 uint32_t cds_atomic_fetch_xor32(void* addr, uint32_t val, int atomic_index, const char * position) {
241         _ATOMIC_RMW_( ^= , 32, addr, val, atomic_index, position);
242 }
243 uint64_t cds_atomic_fetch_xor64(void* addr, uint64_t val, int atomic_index, const char * position) {
244         _ATOMIC_RMW_( ^= , 64, addr, val, atomic_index, position);
245 }
246
247 // cds atomic compare and exchange
248 // In order to accomodate the LLVM PASS, the return values are not true or false. 
249
250 #define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_
251 #define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index, position)                            \
252 ({                                                                                              \
253   uint##size##_t _desired = desired;                                                            \
254   uint##size##_t _expected = expected;                                                          \
255   uint##size##_t _old = model_rmwrcas_action_helper(addr, atomic_index, position);                           \
256   if (_old == _expected) {                                                                    \
257     model_rmw_action_helper(addr, (uint64_t) _desired, atomic_index, position); return _expected; }      \
258   else {                                                                                        \
259     model_rmwc_action_helper(addr, atomic_index, position); _expected = _old; return _old; }              \
260 })
261
262 // atomic_compare_exchange version 1: the CmpOperand (corresponds to expected)
263 // extracted from LLVM IR is an integer type. 
264
265 uint8_t cds_atomic_compare_exchange8_v1(void* addr, uint8_t expected, uint8_t desired, 
266                         int atomic_index_succ, int atomic_index_fail, const char *position )
267 {
268         _ATOMIC_CMPSWP_(8, addr, expected, desired, 
269                                 atomic_index_succ, position);
270 }
271 uint16_t cds_atomic_compare_exchange16_v1(void* addr, uint16_t expected, uint16_t desired, 
272                         int atomic_index_succ, int atomic_index_fail, const char *position)
273 {
274         _ATOMIC_CMPSWP_(16, addr, expected, desired, 
275                                 atomic_index_succ, position);
276 }
277 uint32_t cds_atomic_compare_exchange32_v1(void* addr, uint32_t expected, uint32_t desired, 
278                         int atomic_index_succ, int atomic_index_fail, const char *position)
279 {
280         _ATOMIC_CMPSWP_(32, addr, expected, desired, 
281                                 atomic_index_succ, position);
282 }
283 uint64_t cds_atomic_compare_exchange64_v1(void* addr, uint64_t expected, uint64_t desired, 
284                         int atomic_index_succ, int atomic_index_fail, const char *position)
285 {
286         _ATOMIC_CMPSWP_(64, addr, expected, desired, 
287                                 atomic_index_succ, position);
288 }
289
290 // atomic_compare_exchange version 2
291 bool cds_atomic_compare_exchange8_v2(void* addr, uint8_t* expected, uint8_t desired, 
292                 int atomic_index_succ, int atomic_index_fail, const char *position )
293 {
294         uint8_t ret = cds_atomic_compare_exchange8_v1(addr, *expected,
295                         desired, atomic_index_succ, atomic_index_fail, position);
296         if (ret == *expected) return true;
297         else return false; 
298 }
299 bool cds_atomic_compare_exchange16_v2(void* addr, uint16_t* expected, uint16_t desired, 
300                 int atomic_index_succ, int atomic_index_fail, const char *position)
301 {
302         uint16_t ret = cds_atomic_compare_exchange16_v1(addr, *expected,
303                         desired, atomic_index_succ, atomic_index_fail, position);
304         if (ret == *expected) return true;
305         else return false; 
306 }
307 bool cds_atomic_compare_exchange32_v2(void* addr, uint32_t* expected, uint32_t desired, 
308                 int atomic_index_succ, int atomic_index_fail, const char *position)
309 {
310         uint32_t ret = cds_atomic_compare_exchange32_v1(addr, *expected,
311                         desired, atomic_index_succ, atomic_index_fail, position);
312         if (ret == *expected) return true;
313         else return false; 
314 }
315 bool cds_atomic_compare_exchange64_v2(void* addr, uint64_t* expected, uint64_t desired, 
316                 int atomic_index_succ, int atomic_index_fail, const char *position)
317 {
318         uint64_t ret = cds_atomic_compare_exchange64_v1(addr, *expected,
319                         desired, atomic_index_succ, atomic_index_fail, position);
320         if (ret == *expected) return true;
321         else return false; 
322 }
323
324
325 // cds atomic thread fence
326
327 void cds_atomic_thread_fence(int atomic_index, const char * position) {
328         model->switch_to_master(
329                 new ModelAction(ATOMIC_FENCE, position, orders[atomic_index], FENCE_LOCATION)
330         );
331 }
332
333 /*
334 #define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ )                         \
335         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
336                 __typeof__(__e__) __q__ = (__e__);                            \
337                 __typeof__(__m__) __v__ = (__m__);                            \
338                 bool __r__;                                                   \
339                 __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
340                 if (__t__ == * __q__ ) {                                      \
341                         model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
342                 else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
343                 __r__; })
344
345 #define _ATOMIC_FENCE_( __x__ ) \
346         ({ model_fence_action(__x__);})
347 */
348
349 /*
350
351 #define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ )                         \
352         ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
353         __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
354         __typeof__(__m__) __v__ = (__m__);                                    \
355         __typeof__((__a__)->__f__) __copy__= __old__;                         \
356         __copy__ __o__ __v__;                                                 \
357         model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);          \
358         __old__ = __old__;  Silence clang (-Wunused-value)                    \
359          })                           
360 */