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