LXR linux/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h

   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