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

   1 #ifndef BARRIERS_H
   2 #define BARRIERS_H
   3
   4 #define barrier() __asm__ __volatile__("" : : : "memory")
   5
   6 #ifdef RUN
   7 #define smp_mb() __sync_synchronize()
   8 #define smp_mb__after_unlock_lock() __sync_synchronize()
   9 #else
  10 /*
  11  * Copied from CBMC's implementation of __sync_synchronize(), which
  12  * seems to be disabled by default.
  13  */
  14 #define smp_mb() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \
  15                                  "WWcumul", "RRcumul", "RWcumul", "WRcumul")
  16 #define smp_mb__after_unlock_lock() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \
  17                                     "WWcumul", "RRcumul", "RWcumul", "WRcumul")
  18 #endif
  19
  20 /*
  21  * Allow memory barriers to be disabled in either the read or write side
  22  * of SRCU individually.
  23  */
  24
  25 #ifndef NO_SYNC_SMP_MB
  26 #define sync_smp_mb() smp_mb()
  27 #else
  28 #define sync_smp_mb() do {} while (0)
  29 #endif
  30
  31 #ifndef NO_READ_SIDE_SMP_MB
  32 #define rs_smp_mb() smp_mb()
  33 #else
  34 #define rs_smp_mb() do {} while (0)
  35 #endif
  36
  37 #define ACCESS_ONCE(x) (*(volatile typeof(x) *) &(x))
  38 #define READ_ONCE(x) ACCESS_ONCE(x)
  39 #define WRITE_ONCE(x, val) (ACCESS_ONCE(x) = (val))
  40
  41 #endif