6 #include "snapshot-interface.h"
7 #include "threads-model.h"
9 memory_order orders[6] = {
10 memory_order_relaxed, memory_order_consume, memory_order_acquire,
11 memory_order_release, memory_order_acq_rel, memory_order_seq_cst
14 static void ensureModel(ModelAction * action) {
17 snapshot_system_init(10000, 1024, 1024, 40000);
18 model_init = new ModelChecker();
20 model_init->get_execution()->check_current_action(action);
22 model->switch_to_master(action);
26 /** Performs a read action.*/
27 uint64_t model_read_action(void * obj, memory_order ord) {
28 return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
31 /** Performs a write action.*/
32 void model_write_action(void * obj, memory_order ord, uint64_t val) {
33 model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val));
36 /** Performs an init action. */
37 void model_init_action(void * obj, uint64_t val) {
38 model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
42 * Performs the read part of a RMW action. The next action must either be the
43 * write part of the RMW action or an explicit close out of the RMW action w/o
46 uint64_t model_rmwr_action(void *obj, memory_order ord) {
47 return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
51 * Performs the read part of a RMW CAS action. The next action must
52 * either be the write part of the RMW action or an explicit close out
53 * of the RMW action w/o a write.
55 uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) {
56 return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size));
60 /** Performs the write part of a RMW action. */
61 void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
62 model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
65 /** Closes out a RMW action without doing a write. */
66 void model_rmwc_action(void *obj, memory_order ord) {
67 model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
70 /** Issues a fence operation. */
71 void model_fence_action(memory_order ord) {
72 model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
75 /* --- helper functions --- */
76 uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
77 return model->switch_to_master(
78 new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj)
82 uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
83 return model->switch_to_master(
84 new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)
88 void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) {
89 model->switch_to_master(
90 new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)
94 void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) {
95 model->switch_to_master(
96 new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)
101 void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
103 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
106 void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
108 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
111 void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
113 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
116 void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
118 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
124 uint8_t cds_atomic_load8(void * obj, int atomic_index, const char * position) {
125 return (uint8_t) ( model->switch_to_master(
126 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
129 uint16_t cds_atomic_load16(void * obj, int atomic_index, const char * position) {
130 return (uint16_t) ( model->switch_to_master(
131 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
134 uint32_t cds_atomic_load32(void * obj, int atomic_index, const char * position) {
135 return (uint32_t) ( model->switch_to_master(
136 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
139 uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) {
140 return model->switch_to_master(
141 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)
146 void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
148 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
151 void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
153 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
156 void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
158 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
161 void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
163 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
167 #define _ATOMIC_RMW_(__op__, size, addr, val, atomic_index, position) \
169 uint ## size ## _t _old = model_rmwr_action_helper(addr, atomic_index, position); \
170 uint ## size ## _t _copy = _old; \
171 uint ## size ## _t _val = val; \
173 model_rmw_action_helper(addr, (uint64_t) _copy, atomic_index, position); \
177 // cds atomic exchange
178 uint8_t cds_atomic_exchange8(void* addr, uint8_t val, int atomic_index, const char * position) {
179 _ATOMIC_RMW_( =, 8, addr, val, atomic_index, position);
181 uint16_t cds_atomic_exchange16(void* addr, uint16_t val, int atomic_index, const char * position) {
182 _ATOMIC_RMW_( =, 16, addr, val, atomic_index, position);
184 uint32_t cds_atomic_exchange32(void* addr, uint32_t val, int atomic_index, const char * position) {
185 _ATOMIC_RMW_( =, 32, addr, val, atomic_index, position);
187 uint64_t cds_atomic_exchange64(void* addr, uint64_t val, int atomic_index, const char * position) {
188 _ATOMIC_RMW_( =, 64, addr, val, atomic_index, position);
191 // cds atomic fetch add
192 uint8_t cds_atomic_fetch_add8(void* addr, uint8_t val, int atomic_index, const char * position) {
193 _ATOMIC_RMW_( +=, 8, addr, val, atomic_index, position);
195 uint16_t cds_atomic_fetch_add16(void* addr, uint16_t val, int atomic_index, const char * position) {
196 _ATOMIC_RMW_( +=, 16, addr, val, atomic_index, position);
198 uint32_t cds_atomic_fetch_add32(void* addr, uint32_t val, int atomic_index, const char * position) {
199 _ATOMIC_RMW_( +=, 32, addr, val, atomic_index, position);
201 uint64_t cds_atomic_fetch_add64(void* addr, uint64_t val, int atomic_index, const char * position) {
202 _ATOMIC_RMW_( +=, 64, addr, val, atomic_index, position);
205 // cds atomic fetch sub
206 uint8_t cds_atomic_fetch_sub8(void* addr, uint8_t val, int atomic_index, const char * position) {
207 _ATOMIC_RMW_( -=, 8, addr, val, atomic_index, position);
209 uint16_t cds_atomic_fetch_sub16(void* addr, uint16_t val, int atomic_index, const char * position) {
210 _ATOMIC_RMW_( -=, 16, addr, val, atomic_index, position);
212 uint32_t cds_atomic_fetch_sub32(void* addr, uint32_t val, int atomic_index, const char * position) {
213 _ATOMIC_RMW_( -=, 32, addr, val, atomic_index, position);
215 uint64_t cds_atomic_fetch_sub64(void* addr, uint64_t val, int atomic_index, const char * position) {
216 _ATOMIC_RMW_( -=, 64, addr, val, atomic_index, position);
219 // cds atomic fetch and
220 uint8_t cds_atomic_fetch_and8(void* addr, uint8_t val, int atomic_index, const char * position) {
221 _ATOMIC_RMW_( &=, 8, addr, val, atomic_index, position);
223 uint16_t cds_atomic_fetch_and16(void* addr, uint16_t val, int atomic_index, const char * position) {
224 _ATOMIC_RMW_( &=, 16, addr, val, atomic_index, position);
226 uint32_t cds_atomic_fetch_and32(void* addr, uint32_t val, int atomic_index, const char * position) {
227 _ATOMIC_RMW_( &=, 32, addr, val, atomic_index, position);
229 uint64_t cds_atomic_fetch_and64(void* addr, uint64_t val, int atomic_index, const char * position) {
230 _ATOMIC_RMW_( &=, 64, addr, val, atomic_index, position);
233 // cds atomic fetch or
234 uint8_t cds_atomic_fetch_or8(void* addr, uint8_t val, int atomic_index, const char * position) {
235 _ATOMIC_RMW_( |=, 8, addr, val, atomic_index, position);
237 uint16_t cds_atomic_fetch_or16(void* addr, uint16_t val, int atomic_index, const char * position) {
238 _ATOMIC_RMW_( |=, 16, addr, val, atomic_index, position);
240 uint32_t cds_atomic_fetch_or32(void* addr, uint32_t val, int atomic_index, const char * position) {
241 _ATOMIC_RMW_( |=, 32, addr, val, atomic_index, position);
243 uint64_t cds_atomic_fetch_or64(void* addr, uint64_t val, int atomic_index, const char * position) {
244 _ATOMIC_RMW_( |=, 64, addr, val, atomic_index, position);
247 // cds atomic fetch xor
248 uint8_t cds_atomic_fetch_xor8(void* addr, uint8_t val, int atomic_index, const char * position) {
249 _ATOMIC_RMW_( ^=, 8, addr, val, atomic_index, position);
251 uint16_t cds_atomic_fetch_xor16(void* addr, uint16_t val, int atomic_index, const char * position) {
252 _ATOMIC_RMW_( ^=, 16, addr, val, atomic_index, position);
254 uint32_t cds_atomic_fetch_xor32(void* addr, uint32_t val, int atomic_index, const char * position) {
255 _ATOMIC_RMW_( ^=, 32, addr, val, atomic_index, position);
257 uint64_t cds_atomic_fetch_xor64(void* addr, uint64_t val, int atomic_index, const char * position) {
258 _ATOMIC_RMW_( ^=, 64, addr, val, atomic_index, position);
261 // cds atomic compare and exchange
262 // In order to accomodate the LLVM PASS, the return values are not true or false.
264 #define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_
265 #define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index, position) \
267 uint ## size ## _t _desired = desired; \
268 uint ## size ## _t _expected = expected; \
269 uint ## size ## _t _old = model_rmwrcas_action_helper(addr, atomic_index, _expected, sizeof(_expected), position); \
270 if (_old == _expected) { \
271 model_rmw_action_helper(addr, (uint64_t) _desired, atomic_index, position); return _expected; } \
273 model_rmwc_action_helper(addr, atomic_index, position); _expected = _old; return _old; } \
276 // atomic_compare_exchange version 1: the CmpOperand (corresponds to expected)
277 // extracted from LLVM IR is an integer type.
279 uint8_t cds_atomic_compare_exchange8_v1(void* addr, uint8_t expected, uint8_t desired,
280 int atomic_index_succ, int atomic_index_fail, const char *position )
282 _ATOMIC_CMPSWP_(8, addr, expected, desired,
283 atomic_index_succ, position);
285 uint16_t cds_atomic_compare_exchange16_v1(void* addr, uint16_t expected, uint16_t desired,
286 int atomic_index_succ, int atomic_index_fail, const char *position)
288 _ATOMIC_CMPSWP_(16, addr, expected, desired,
289 atomic_index_succ, position);
291 uint32_t cds_atomic_compare_exchange32_v1(void* addr, uint32_t expected, uint32_t desired,
292 int atomic_index_succ, int atomic_index_fail, const char *position)
294 _ATOMIC_CMPSWP_(32, addr, expected, desired,
295 atomic_index_succ, position);
297 uint64_t cds_atomic_compare_exchange64_v1(void* addr, uint64_t expected, uint64_t desired,
298 int atomic_index_succ, int atomic_index_fail, const char *position)
300 _ATOMIC_CMPSWP_(64, addr, expected, desired,
301 atomic_index_succ, position);
304 // atomic_compare_exchange version 2
305 bool cds_atomic_compare_exchange8_v2(void* addr, uint8_t* expected, uint8_t desired,
306 int atomic_index_succ, int atomic_index_fail, const char *position )
308 uint8_t ret = cds_atomic_compare_exchange8_v1(addr, *expected,
309 desired, atomic_index_succ, atomic_index_fail, position);
310 if (ret == *expected) return true;
313 bool cds_atomic_compare_exchange16_v2(void* addr, uint16_t* expected, uint16_t desired,
314 int atomic_index_succ, int atomic_index_fail, const char *position)
316 uint16_t ret = cds_atomic_compare_exchange16_v1(addr, *expected,
317 desired, atomic_index_succ, atomic_index_fail, position);
318 if (ret == *expected) return true;
321 bool cds_atomic_compare_exchange32_v2(void* addr, uint32_t* expected, uint32_t desired,
322 int atomic_index_succ, int atomic_index_fail, const char *position)
324 uint32_t ret = cds_atomic_compare_exchange32_v1(addr, *expected,
325 desired, atomic_index_succ, atomic_index_fail, position);
326 if (ret == *expected) return true;
329 bool cds_atomic_compare_exchange64_v2(void* addr, uint64_t* expected, uint64_t desired,
330 int atomic_index_succ, int atomic_index_fail, const char *position)
332 uint64_t ret = cds_atomic_compare_exchange64_v1(addr, *expected,
333 desired, atomic_index_succ, atomic_index_fail, position);
334 if (ret == *expected) return true;
339 // cds atomic thread fence
341 void cds_atomic_thread_fence(int atomic_index, const char * position) {
342 model->switch_to_master(
343 new ModelAction(ATOMIC_FENCE, position, orders[atomic_index], FENCE_LOCATION)
348 #define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ ) \
349 ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); \
350 __typeof__(__e__) __q__ = (__e__); \
351 __typeof__(__m__) __v__ = (__m__); \
353 __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
354 if (__t__ == * __q__ ) { \
355 model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
356 else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \
359 #define _ATOMIC_FENCE_( __x__ ) \
360 ({ model_fence_action(__x__);})
365 #define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ ) \
366 ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); \
367 __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
368 __typeof__(__m__) __v__ = (__m__); \
369 __typeof__((__a__)->__f__) __copy__= __old__; \
370 __copy__ __o__ __v__; \
371 model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); \
372 __old__ = __old__; Silence clang (-Wunused-value) \