summaryrefslogtreecommitdiff
path: root/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h
blob: 3f95a768a03b45c4fc32393297a4ed6af88145d6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
/* SPDX-License-Identifier: GPL-2.0 */
#ifndef BARRIERS_H
#define BARRIERS_H

#define barrier() __asm__ __volatile__("" : : : "memory")

#ifdef RUN
#define smp_mb() __sync_synchronize()
#define smp_mb__after_unlock_lock() __sync_synchronize()
#else
/*
 * Copied from CBMC's implementation of __sync_synchronize(), which
 * seems to be disabled by default.
 */
#define smp_mb() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \
				 "WWcumul", "RRcumul", "RWcumul", "WRcumul")
#define smp_mb__after_unlock_lock() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \
				    "WWcumul", "RRcumul", "RWcumul", "WRcumul")
#endif

/*
 * Allow memory barriers to be disabled in either the read or write side
 * of SRCU individually.
 */

#ifndef NO_SYNC_SMP_MB
#define sync_smp_mb() smp_mb()
#else
#define sync_smp_mb() do {} while (0)
#endif

#ifndef NO_READ_SIDE_SMP_MB
#define rs_smp_mb() smp_mb()
#else
#define rs_smp_mb() do {} while (0)
#endif

#define READ_ONCE(x) (*(volatile typeof(x) *) &(x))
#define WRITE_ONCE(x) ((*(volatile typeof(x) *) &(x)) = (val))

#endif