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

INCLUDED FROM

   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