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