RFC: linux-aarch64 and LSE support

[Andrew Haley]

On 9/23/22 00:40, dean.long at oracle.com wrote:
 > Also, since "Barrier-ordered-before" describes when RW1 "happened
 > before" RW2 (or RW2 "happened after" RW1, right?), I don't understand
 > why an additional "barrier-ordered-after" would be desired.

This was explained by the comment:

   // This was checked by using the herd7 consistency model simulator
   // (http://diy.inria.fr/) with this test case:
   //
   // AArch64 LseCas
   // { 0:X1=x; 0:X2=y; 1:X1=x; 1:X2=y; }
   // P0 | P1;
   // LDR W4, [X2] | MOV W3, #0;
   // DMB LD       | MOV W4, #1;
   // LDR W3, [X1] | CASAL W3, W4, [X1];
   //              | DMB ISH;
   //              | STR W4, [X2];
   // exists
   // (0:X3=0 /\ 0:X4=1)

Here, if you remove the trailing DMB the store to [x2] has become visible
before the store to [x1].

This happens because the CASAL followed by the STR has the memory effect of

   load [x1]; acquire; release; store [x1]; store [x2]

And it's obvious that there is no ordering between the two stores. The
fact that the operation on [x1] is atomic has no bearing on when the
stores to [x1] and [x2] become visible.

In order to prevent this reordering, we need StoreStore|StoreLoad after
the CASAL.

It's very instructive to run this test on the consistency model simulator.
This interpretation was confirmed by the author of the Arm memory model.

HOWEVER, the spec has been changed again, and it may well be that we no
longer need the trailing barrier, because of the section you quoted:

   A memory read or write effect RW1 is Barrier-ordered-before a memory
   read or write effect RW2 from the same Observer if and only if RW1
   appears in program order before RW2 and any of the following cases
   apply:

    • RW1 is a memory write effect W1 and is generated by an atomic
      instruction with both Acquire and Release semantics.

... which looks like the spec has been tightened enough that we do not
need the trailing barrier. Having said that, I think we still may need
it for non-LSE, at least in theory.

-- 
Andrew Haley  (he/him)
Java Platform Lead Engineer
Red Hat UK Ltd. <https://www.redhat.com>
https://keybase.io/andrewhaley
EAC8 43EB D3EF DB98 CC77 2FAD A5CD 6035 332F A671