| /* SPDX-License-Identifier: GPL-2.0 */ |
| #define barrier() __asm__ __volatile__("" : : : "memory") |
| #define smp_mb() __sync_synchronize() |
| #define smp_mb__after_unlock_lock() __sync_synchronize() |
| * 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") |
| * Allow memory barriers to be disabled in either the read or write side |
| #define sync_smp_mb() smp_mb() |
| #define sync_smp_mb() do {} while (0) |
| #ifndef NO_READ_SIDE_SMP_MB |
| #define rs_smp_mb() smp_mb() |
| #define rs_smp_mb() do {} while (0) |
| #define READ_ONCE(x) (*(volatile typeof(x) *) &(x)) |
| #define WRITE_ONCE(x) ((*(volatile typeof(x) *) &(x)) = (val)) |