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

#ifndef BARRIERS_H

#define BARRIERS_H


#define barrier() __asm__ __volatile__("" : : : "memory")

#ifdef RUN

#define smp_mb() __sync_synchronize()

#define smp_mb__after_unlock_lock() __sync_synchronize()
#else
/*
 * 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")
#endif

/*
 * Allow memory barriers to be disabled in either the read or write side
 * of SRCU individually.
 */

#ifndef NO_SYNC_SMP_MB

#define sync_smp_mb() smp_mb()
#else

#define sync_smp_mb() do {} while (0)
#endif

#ifndef NO_READ_SIDE_SMP_MB

#define rs_smp_mb() smp_mb()
#else

#define rs_smp_mb() do {} while (0)
#endif


#define ACCESS_ONCE(x) (*(volatile typeof(x) *) &(x))

#define READ_ONCE(x) ACCESS_ONCE(x)

#define WRITE_ONCE(x, val) (ACCESS_ONCE(x) = (val))

#endif
Overall Contributors
Person
Tokens
Prop
Commits
CommitProp
Lance Roy
99
100.00%
1
100.00%
Total
99
100.00%
1
100.00%
Directory: tools/testing/selftests/rcutorture/formal/srcu-cbmc/src

Information contained on this website is for historical information purposes only and does not indicate or represent copyright ownership.