33 lines
508 B
Plaintext
33 lines
508 B
Plaintext
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)
|