On Thu, 2 Nov 2017, Andrea Parri wrote:
> > This is forbidden. It would remain forbidden even if the smp_mb in P1
> > were replaced by a similar release/acquire pair for the same memory
> > location.
>
> Hopefully, the LKMM does not agree with this assessment... ;-)
No, it doesn't.
> Here's a two-threads example showing that "(w)mb is _not_ rfi-rel-acq":
>
> C rfi-rel-acq-is-not-mb
>
> {}
>
> P0(int *x, int *y, int *a)
> {
> WRITE_ONCE(*x, 1);
> smp_store_release(a, 1);
> r1 = smp_load_acquire(a);
> WRITE_ONCE(*y, 1);
> }
>
> P1(int *x, int *y)
> {
> int r0;
> int r1;
>
> r0 = READ_ONCE(*y);
> smp_rmb();
> r1 = READ_ONCE(*x);
> }
>
> exists (1:r0=1 /\ 1:r1=0)
Right. There is a happens-before edge between the two WRITE_ONCE calls
in P0 but no cumul-fence edge, and therefore the test is allowed.
Here is an example where a happens-before edge suffices to provide
ordering:
P0(int *x, int *y)
{
WRITE_ONCE(*x, 1);
smp_wmb();
WRITE_ONCE(*y, 1);
}
P1(int *x, int *y, int *a)
{
int rx, ry, ra;
ry = READ_ONCE(*y);
smp_store_release(a, 1);
ra = smp_load_acquire(a);
rx = READ_ONCE(*x);
}
exists (1:rx=0 /\ 1:ry=1)
This test is forbidden, but it would be allowed if the release and
acquire accessed different locations.
Alan Stern
