On Mon, Sep 21, 2015 at 03:10:38PM +0100, Boqun Feng wrote:

On Mon, Sep 21, 2015 at 09:45:15PM +0800, Boqun Feng wrote:

quoted

On Thu, Sep 17, 2015 at 07:00:01PM +0100, Will Deacon wrote:

quoted

On Thu, Sep 17, 2015 at 03:50:12AM +0100, Boqun Feng wrote:

quoted

If an ACQUIRE loads the value of stored by a RELEASE, then after the
ACQUIRE operation, the CPU executing the ACQUIRE operation will perceive
all the memory operations that have been perceived by the CPU executing
the RELEASE operation before the RELEASE operation. 

Which means a release+acquire pair to the same variable guarantees
transitivity.

Almost, but on arm64 at least, "all the memory operations" above doesn't
include reads by other CPUs. I'm struggling to figure out whether that's
actually an issue.

Ah.. that's indeed an issue! for example:

CPU 0			CPU 1				CPU 2
=====================	==========================	================
{a = 0, b = 0, c = 0}
r1 = READ_ONCE(a);	WRITE_ONCE(b, 1);		r3 = smp_load_acquire(&c);
smp_rmb();		smp_store_release(&c, 1);	WRITE_ONCE(a, 1);
r2 = READ_ONCE(b)

where r1 == 1 && r2 == 0 && r3 == 1 is actually not prohibitted, at
least on POWER.

Oops.. I use wrong litmus here.. so this is prohibitted on POWER. Sorry
for the misleading. How about the behavior of that on arm and arm64?

That explicit test is forbidden on arm/arm64 because of the smp_rmb(),
but if you rewrite it as (LDAR is acquire, STLR is release):


  {
  0:X1=x; 0:X3=y;
  1:X1=y; 1:X2=z;
  2:X1=z; 2:X3=x;
  }
   P0           | P1           | P2                ;
   LDAR W0,[X1] | MOV W0,#1    | LDAR W0,[X1]      ;
   LDR W2,[X3]  | STR W0,[X1]  | MOV W2,#1         ;
                | STLR W0,[X2] | STR W2,[X3]       ;

  Observed
      0:X0=1; 0:X2=0; 2:X0=1;


then it is permitted on arm64. Note that herd currently claims that this
is forbidden, but I'm talking to the authors about getting that fixed :)

Will