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