| C Atomic-RMW+mb__after_atomic-is-stronger-than-acquire | |
| (* | |
| * Result: Never | |
| * | |
| * Test that an atomic RMW followed by a smp_mb__after_atomic() is | |
| * stronger than a normal acquire: both the read and write parts of | |
| * the RMW are ordered before the subsequential memory accesses. | |
| *) | |
| { | |
| } | |
| P0(int *x, atomic_t *y) | |
| { | |
| int r0; | |
| int r1; | |
| r0 = READ_ONCE(*x); | |
| smp_rmb(); | |
| r1 = atomic_read(y); | |
| } | |
| P1(int *x, atomic_t *y) | |
| { | |
| atomic_inc(y); | |
| smp_mb__after_atomic(); | |
| WRITE_ONCE(*x, 1); | |
| } | |
| exists | |
| (0:r0=1 /\ 0:r1=0) |