9 #include "snapshot-interface.h"
10 #include "threads-model.h"
12 memory_order orders[6] = {
13 memory_order_relaxed, memory_order_consume, memory_order_acquire,
14 memory_order_release, memory_order_acq_rel, memory_order_seq_cst
17 #define ensureModel(action) \
18 if (!modelchecker_started) { \
20 snapshot_system_init(10000, 1024, 1024, 40000); \
21 model = new ModelChecker(); \
23 model->get_execution()->check_current_action(action); \
25 model->switch_to_master(action); \
29 #define ensureModelValue(action, type) \
30 if (!modelchecker_started) { \
32 snapshot_system_init(10000, 1024, 1024, 40000); \
33 model = new ModelChecker(); \
35 model->get_execution()->check_current_action(action); \
36 return (type) thread_current()->get_return_value(); \
38 return (type) model->switch_to_master(action); \
41 /** Performs a read action.*/
42 uint64_t model_read_action(void * obj, memory_order ord) {
43 return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
46 /** Performs a write action.*/
47 void model_write_action(void * obj, memory_order ord, uint64_t val) {
48 model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val));
51 /** Performs an init action. */
52 void model_init_action(void * obj, uint64_t val) {
53 model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
57 * Performs the read part of a RMW action. The next action must either be the
58 * write part of the RMW action or an explicit close out of the RMW action w/o
61 uint64_t model_rmwr_action(void *obj, memory_order ord) {
62 return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
66 * Performs the read part of a RMW CAS action. The next action must
67 * either be the write part of the RMW action or an explicit close out
68 * of the RMW action w/o a write.
70 uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) {
71 return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size));
75 /** Performs the write part of a RMW action. */
76 void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
77 model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
80 /** Closes out a RMW action without doing a write. */
81 void model_rmwc_action(void *obj, memory_order ord) {
82 model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
85 /** Issues a fence operation. */
86 void model_fence_action(memory_order ord) {
87 model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
90 /* --- helper functions --- */
91 uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
93 new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size), uint64_t
97 uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
98 ensureModelValue(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj), uint64_t);
101 void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) {
102 ensureModel(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val));
105 void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) {
106 ensureModel(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj));
110 void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
112 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
115 void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
117 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
120 void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
122 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
125 void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
127 new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
133 uint8_t cds_atomic_load8(void * obj, int atomic_index, const char * position) {
135 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint8_t);
137 uint16_t cds_atomic_load16(void * obj, int atomic_index, const char * position) {
139 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint16_t);
141 uint32_t cds_atomic_load32(void * obj, int atomic_index, const char * position) {
143 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint32_t
146 uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) {
148 new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint64_t);
152 void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
154 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
157 void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
159 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
162 void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
164 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
167 void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
169 new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
173 #define _ATOMIC_RMW_(__op__, size, addr, val, atomic_index, position) \
175 uint ## size ## _t _old = model_rmwr_action_helper(addr, atomic_index, position); \
176 uint ## size ## _t _copy = _old; \
177 uint ## size ## _t _val = val; \
179 model_rmw_action_helper(addr, (uint64_t) _copy, atomic_index, position); \
183 // cds atomic exchange
184 uint8_t cds_atomic_exchange8(void* addr, uint8_t val, int atomic_index, const char * position) {
185 _ATOMIC_RMW_( =, 8, addr, val, atomic_index, position);
187 uint16_t cds_atomic_exchange16(void* addr, uint16_t val, int atomic_index, const char * position) {
188 _ATOMIC_RMW_( =, 16, addr, val, atomic_index, position);
190 uint32_t cds_atomic_exchange32(void* addr, uint32_t val, int atomic_index, const char * position) {
191 _ATOMIC_RMW_( =, 32, addr, val, atomic_index, position);
193 uint64_t cds_atomic_exchange64(void* addr, uint64_t val, int atomic_index, const char * position) {
194 _ATOMIC_RMW_( =, 64, addr, val, atomic_index, position);
197 // cds atomic fetch add
198 uint8_t cds_atomic_fetch_add8(void* addr, uint8_t val, int atomic_index, const char * position) {
199 _ATOMIC_RMW_( +=, 8, addr, val, atomic_index, position);
201 uint16_t cds_atomic_fetch_add16(void* addr, uint16_t val, int atomic_index, const char * position) {
202 _ATOMIC_RMW_( +=, 16, addr, val, atomic_index, position);
204 uint32_t cds_atomic_fetch_add32(void* addr, uint32_t val, int atomic_index, const char * position) {
205 _ATOMIC_RMW_( +=, 32, addr, val, atomic_index, position);
207 uint64_t cds_atomic_fetch_add64(void* addr, uint64_t val, int atomic_index, const char * position) {
208 _ATOMIC_RMW_( +=, 64, addr, val, atomic_index, position);
211 // cds atomic fetch sub
212 uint8_t cds_atomic_fetch_sub8(void* addr, uint8_t val, int atomic_index, const char * position) {
213 _ATOMIC_RMW_( -=, 8, addr, val, atomic_index, position);
215 uint16_t cds_atomic_fetch_sub16(void* addr, uint16_t val, int atomic_index, const char * position) {
216 _ATOMIC_RMW_( -=, 16, addr, val, atomic_index, position);
218 uint32_t cds_atomic_fetch_sub32(void* addr, uint32_t val, int atomic_index, const char * position) {
219 _ATOMIC_RMW_( -=, 32, addr, val, atomic_index, position);
221 uint64_t cds_atomic_fetch_sub64(void* addr, uint64_t val, int atomic_index, const char * position) {
222 _ATOMIC_RMW_( -=, 64, addr, val, atomic_index, position);
225 // cds atomic fetch and
226 uint8_t cds_atomic_fetch_and8(void* addr, uint8_t val, int atomic_index, const char * position) {
227 _ATOMIC_RMW_( &=, 8, addr, val, atomic_index, position);
229 uint16_t cds_atomic_fetch_and16(void* addr, uint16_t val, int atomic_index, const char * position) {
230 _ATOMIC_RMW_( &=, 16, addr, val, atomic_index, position);
232 uint32_t cds_atomic_fetch_and32(void* addr, uint32_t val, int atomic_index, const char * position) {
233 _ATOMIC_RMW_( &=, 32, addr, val, atomic_index, position);
235 uint64_t cds_atomic_fetch_and64(void* addr, uint64_t val, int atomic_index, const char * position) {
236 _ATOMIC_RMW_( &=, 64, addr, val, atomic_index, position);
239 // cds atomic fetch or
240 uint8_t cds_atomic_fetch_or8(void* addr, uint8_t val, int atomic_index, const char * position) {
241 _ATOMIC_RMW_( |=, 8, addr, val, atomic_index, position);
243 uint16_t cds_atomic_fetch_or16(void* addr, uint16_t val, int atomic_index, const char * position) {
244 _ATOMIC_RMW_( |=, 16, addr, val, atomic_index, position);
246 uint32_t cds_atomic_fetch_or32(void* addr, uint32_t val, int atomic_index, const char * position) {
247 _ATOMIC_RMW_( |=, 32, addr, val, atomic_index, position);
249 uint64_t cds_atomic_fetch_or64(void* addr, uint64_t val, int atomic_index, const char * position) {
250 _ATOMIC_RMW_( |=, 64, addr, val, atomic_index, position);
253 // cds atomic fetch xor
254 uint8_t cds_atomic_fetch_xor8(void* addr, uint8_t val, int atomic_index, const char * position) {
255 _ATOMIC_RMW_( ^=, 8, addr, val, atomic_index, position);
257 uint16_t cds_atomic_fetch_xor16(void* addr, uint16_t val, int atomic_index, const char * position) {
258 _ATOMIC_RMW_( ^=, 16, addr, val, atomic_index, position);
260 uint32_t cds_atomic_fetch_xor32(void* addr, uint32_t val, int atomic_index, const char * position) {
261 _ATOMIC_RMW_( ^=, 32, addr, val, atomic_index, position);
263 uint64_t cds_atomic_fetch_xor64(void* addr, uint64_t val, int atomic_index, const char * position) {
264 _ATOMIC_RMW_( ^=, 64, addr, val, atomic_index, position);
267 // cds atomic compare and exchange
268 // In order to accomodate the LLVM PASS, the return values are not true or false.
270 #define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_
271 #define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index, position) \
273 uint ## size ## _t _desired = desired; \
274 uint ## size ## _t _expected = expected; \
275 uint ## size ## _t _old = model_rmwrcas_action_helper(addr, atomic_index, _expected, sizeof(_expected), position); \
276 if (_old == _expected) { \
277 model_rmw_action_helper(addr, (uint64_t) _desired, atomic_index, position); return _expected; } \
279 model_rmwc_action_helper(addr, atomic_index, position); _expected = _old; return _old; } \
282 // atomic_compare_exchange version 1: the CmpOperand (corresponds to expected)
283 // extracted from LLVM IR is an integer type.
285 uint8_t cds_atomic_compare_exchange8_v1(void* addr, uint8_t expected, uint8_t desired,
286 int atomic_index_succ, int atomic_index_fail, const char *position )
288 _ATOMIC_CMPSWP_(8, addr, expected, desired,
289 atomic_index_succ, position);
291 uint16_t cds_atomic_compare_exchange16_v1(void* addr, uint16_t expected, uint16_t desired,
292 int atomic_index_succ, int atomic_index_fail, const char *position)
294 _ATOMIC_CMPSWP_(16, addr, expected, desired,
295 atomic_index_succ, position);
297 uint32_t cds_atomic_compare_exchange32_v1(void* addr, uint32_t expected, uint32_t desired,
298 int atomic_index_succ, int atomic_index_fail, const char *position)
300 _ATOMIC_CMPSWP_(32, addr, expected, desired,
301 atomic_index_succ, position);
303 uint64_t cds_atomic_compare_exchange64_v1(void* addr, uint64_t expected, uint64_t desired,
304 int atomic_index_succ, int atomic_index_fail, const char *position)
306 _ATOMIC_CMPSWP_(64, addr, expected, desired,
307 atomic_index_succ, position);
310 // atomic_compare_exchange version 2
311 bool cds_atomic_compare_exchange8_v2(void* addr, uint8_t* expected, uint8_t desired,
312 int atomic_index_succ, int atomic_index_fail, const char *position )
314 uint8_t ret = cds_atomic_compare_exchange8_v1(addr, *expected,
315 desired, atomic_index_succ, atomic_index_fail, position);
316 if (ret == *expected) return true;
319 bool cds_atomic_compare_exchange16_v2(void* addr, uint16_t* expected, uint16_t desired,
320 int atomic_index_succ, int atomic_index_fail, const char *position)
322 uint16_t ret = cds_atomic_compare_exchange16_v1(addr, *expected,
323 desired, atomic_index_succ, atomic_index_fail, position);
324 if (ret == *expected) return true;
327 bool cds_atomic_compare_exchange32_v2(void* addr, uint32_t* expected, uint32_t desired,
328 int atomic_index_succ, int atomic_index_fail, const char *position)
330 uint32_t ret = cds_atomic_compare_exchange32_v1(addr, *expected,
331 desired, atomic_index_succ, atomic_index_fail, position);
332 if (ret == *expected) return true;
335 bool cds_atomic_compare_exchange64_v2(void* addr, uint64_t* expected, uint64_t desired,
336 int atomic_index_succ, int atomic_index_fail, const char *position)
338 uint64_t ret = cds_atomic_compare_exchange64_v1(addr, *expected,
339 desired, atomic_index_succ, atomic_index_fail, position);
340 if (ret == *expected) return true;
345 // cds atomic thread fence
347 void cds_atomic_thread_fence(int atomic_index, const char * position) {
348 model->switch_to_master(
349 new ModelAction(ATOMIC_FENCE, position, orders[atomic_index], FENCE_LOCATION)
354 #define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ ) \
355 ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); \
356 __typeof__(__e__) __q__ = (__e__); \
357 __typeof__(__m__) __v__ = (__m__); \
359 __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
360 if (__t__ == * __q__ ) { \
361 model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
362 else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \
365 #define _ATOMIC_FENCE_( __x__ ) \
366 ({ model_fence_action(__x__);})
371 #define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ ) \
372 ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); \
373 __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
374 __typeof__(__m__) __v__ = (__m__); \
375 __typeof__((__a__)->__f__) __copy__= __old__; \
376 __copy__ __o__ __v__; \
377 model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); \
378 __old__ = __old__; Silence clang (-Wunused-value) \
382 void cds_func_entry(const char * funcName) {
385 Thread * th = thread_current();
388 ModelHistory *history = model->get_history();
389 if ( !history->getFuncMap()->contains(funcName) ) {
390 func_id = history->get_func_counter();
391 history->incr_func_counter();
393 history->getFuncMap()->put(funcName, func_id);
395 func_id = history->getFuncMap()->get(funcName);
398 history->enter_function(func_id, th->get_id());
401 void cds_func_exit(const char * funcName) {
404 Thread * th = thread_current();
407 ModelHistory *history = model->get_history();
408 func_id = history->getFuncMap()->get(funcName);
410 history->exit_function(func_id, th->get_id());