33 lines · plain
1C Atomic-RMW+mb__after_atomic-is-stronger-than-acquire2 3(*4 * Result: Never5 *6 * Test that an atomic RMW followed by a smp_mb__after_atomic() is7 * stronger than a normal acquire: both the read and write parts of8 * the RMW are ordered before the subsequential memory accesses.9 *)10 11{12}13 14P0(int *x, atomic_t *y)15{16 int r0;17 int r1;18 19 r0 = READ_ONCE(*x);20 smp_rmb();21 r1 = atomic_read(y);22}23 24P1(int *x, atomic_t *y)25{26 atomic_inc(y);27 smp_mb__after_atomic();28 WRITE_ONCE(*x, 1);29}30 31exists32(0:r0=1 /\ 0:r1=0)33