1 #ifndef BARRIERS_H 2 #define BARRIERS_H 3 4 #define barrier() __asm__ __volatile__("" : : : "memory") 5 6 #ifdef RUN 7 #define smp_mb() __sync_synchronize() 8 #define smp_mb__after_unlock_lock() __sync_synchronize() 9 #else 10 /* 11 * Copied from CBMC's implementation of __sync_synchronize(), which 12 * seems to be disabled by default. 13 */ 14 #define smp_mb() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \ 15 "WWcumul", "RRcumul", "RWcumul", "WRcumul") 16 #define smp_mb__after_unlock_lock() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \ 17 "WWcumul", "RRcumul", "RWcumul", "WRcumul") 18 #endif 19 20 /* 21 * Allow memory barriers to be disabled in either the read or write side 22 * of SRCU individually. 23 */ 24 25 #ifndef NO_SYNC_SMP_MB 26 #define sync_smp_mb() smp_mb() 27 #else 28 #define sync_smp_mb() do {} while (0) 29 #endif 30 31 #ifndef NO_READ_SIDE_SMP_MB 32 #define rs_smp_mb() smp_mb() 33 #else 34 #define rs_smp_mb() do {} while (0) 35 #endif 36 37 #define ACCESS_ONCE(x) (*(volatile typeof(x) *) &(x)) 38 #define READ_ONCE(x) ACCESS_ONCE(x) 39 #define WRITE_ONCE(x, val) (ACCESS_ONCE(x) = (val)) 40 41 #endif 42
