Re: [PATCH] barriers: introduce smp_mb__release_acquire and update documentation

[Will Deacon <will.deacon@arm.com>]

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:
> > On Thu, Sep 17, 2015 at 07:00:01PM +0100, Will Deacon wrote:
> > > On Thu, Sep 17, 2015 at 03:50:12AM +0100, Boqun Feng wrote:
> > > > 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