[PATCH] D141748: [WoA] Use fences for sequentially consistent stores/writes

[John Brawn via Phabricator via llvm-commits]

john.brawn added a comment.

It looks like if MSVC is implementing sequentially-consistent atomic operations in the manner described then we will need to stores (but not loads) in the same way, so it looks like this patch is doing the right thing. Reasoning below:

Using the memory model simulator at http://diy.inria.fr/www/?record=aarch64, the following input has three threads purely using LDAR/STRL

  AArch64 SeqCst
  {
  0:X1=x; 1:X1=x; 2:X1=x;
  0:X3=y; 1:X3=y; 2:X3=y;
  }
   P0            | P1            | P2 ;
   MOV W0, #1    | MOV W2, #1    | LDAR W2, [X3] ;
   STLR W0, [X1] | STLR W2, [X3] | LDAR W0, [X1] ;
   LDAR W2, [X3] | LDAR W0, [X1] | ;
  exists(2:X2=1 /\ 2:X0=0 /\ 0:X2=0 /\ 1:X0=1)

gives the result "No", which means it's not possible for `P2` to see X2=1 and X0=0 if `P0` sees X2=0 and `P1` sees X0=1, or in other words using LDAR/STRL gives sequentially consistent behaviour.

The following has thread P0 do STLR followed by a MSVC-style sequentially consistent load

  AArch64 SeqCst
  {
  0:X1=x; 1:X1=x; 2:X1=x;
  0:X3=y; 1:X3=y; 2:X3=y;
  }
   P0            | P1            | P2 ;
   MOV W0, #1    | MOV W2, #1    | LDAR W2, [X3] ;
   STLR W0, [X1] | STLR W2, [X3] | LDAR W0, [X1] ;
   LDR W2, [X3]  | LDAR W0, [X1] | ;
   DMB ISH       |               | ;
  exists(2:X2=1 /\ 2:X0=0 /\ 0:X2=0 /\ 1:X0=1)

this gives the result "OK", meaning it is possible for these threads to observe that, which means that we don't have sequentially consistent behaviour.

For the MSVC-style sequentially consistent store followed by LDAR

  AArch64 SeqCst
  {
  0:X1=x; 1:X1=x; 2:X1=x;
  0:X3=y; 1:X3=y; 2:X3=y;
  }
   P0            | P1            | P2 ;
   MOV W0, #1    | MOV W2, #1    | LDAR W2, [X3] ;
   DMB ISH       |               | ;
   STR W0, [X1]  | STLR W2, [X3] | LDAR W0, [X1] ;
   DMB ISH       |               | ;
   LDAR W2, [X3] | LDAR W0, [X1] | ;
  exists(2:X2=1 /\ 2:X0=0 /\ 0:X2=0 /\ 1:X0=1)

we get "No", so we still do get sequentially consistent behaviour in this case.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D141748/new/

https://reviews.llvm.org/D141748