]>
Commit | Line | Data |
---|---|---|
b2441318 | 1 | /* SPDX-License-Identifier: GPL-2.0 */ |
418b2977 LR |
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 ACCESS_ONCE(x) (*(volatile typeof(x) *) &(x)) | |
39 | #define READ_ONCE(x) ACCESS_ONCE(x) | |
40 | #define WRITE_ONCE(x, val) (ACCESS_ONCE(x) = (val)) | |
41 | ||
42 | #endif |