RFR: 8262519: AArch64: Unnecessary acquire semantics of memory-order-conservative atomics in C++ Hotspot code

[Dong Bo]

On Thu, 4 Mar 2021 14:23:34 GMT, Andrew Haley <aph at openjdk.org> wrote:

> ```
> AArch64 SeqCst
> { 0:X0=a; 0:X1=b; 1:X0=a; 1:X1=b; a=0; b=0; }
> P0 | P1;
> MOV W3, #1          | MOV W3, #1;
> MOV W8, #99         | MOV W8, #99 ;
> STR W3, [X0]        | STR W3, [X1];
> LDXR W2, [X1]       | LDXR W2, [X0];
> STLXR W5, W8, [X1]  | STLXR W5, W8, [X0]  ;
> CBZ W5, FOO         | CBZ W5, FOO1        ;
> MOV W2, #1234       | MOV W2, #1234        ;
> FOO:                | FOO1:               ;
> DMB ST              | DMB ST             ;
> exists
> (0:X2=0 /\ 1:X2 = 0)
> 
> Test SeqCst Allowed
> States 8
> 0:X2=0; 1:X2=1;
> 0:X2=0; 1:X2=1234;
> 0:X2=1; 1:X2=0;
> 0:X2=1; 1:X2=1;
> 0:X2=1; 1:X2=1234;
> 0:X2=1234; 1:X2=0;
> 0:X2=1234; 1:X2=1;
> 0:X2=1234; 1:X2=1234;
> No
> Witnesses
> Positive: 0 Negative: 15
> Condition exists (0:X2=0 /\ 1:X2=0)
> Observation SeqCst Never 0 15
> ```

Yes, if either preceding store in the two threads can reorder with `ldxr`, the exist condition would be satisfied.
Seems this test can also be extended to verify the order of preceding loads:
AArch64 SeqCst
{ 0:X0=a; 0:X1=b; 0:X10=c; 0:X11=d;
  1:X0=a; 1:X1=b; 1:X10=c; 1:X11=d;
  a=0;    b=0;    c=0;     d=0 }
P0                  | P1                 ;
MOV W3, #1          | MOV W3, #1         ;
MOV W8, #99         | MOV W8, #99        ;
MOV W9, #9          | MOV W9, #9         ;
STR W3, [X0]        | STR W3, [X1]       ;
STLR W9, [X10]      | STLR W9, [X11]     ;
LDR W7, [X11]       | LDR W7, [X10]      ;
LDXR W2, [X1]       | LDXR W2, [X0]      ;
STLXR W5, W8, [X1]  | STLXR W5, W8, [X0] ;
CBZ W5, FOO         | CBZ W5, FOO1       ;
MOV W2, #1234       | MOV W2, #1234      ;
FOO:                | FOO1:              ;
DMB ST              | DMB ST             ;
exists((0:X2=0 /\ 0:X7=9) / (1:X2=0 /\ 1:X7=9))

Test SeqCst Allowed
States 24
0:X2=0; 0:X7=0; 1:X2=1; 1:X7=0;
0:X2=0; 0:X7=0; 1:X2=1; 1:X7=9;
0:X2=0; 0:X7=0; 1:X2=1234; 1:X7=0;
0:X2=0; 0:X7=0; 1:X2=1234; 1:X7=9;
0:X2=1; 0:X7=0; 1:X2=0; 1:X7=0;
0:X2=1; 0:X7=0; 1:X2=1; 1:X7=0;
0:X2=1; 0:X7=0; 1:X2=1; 1:X7=9;
0:X2=1; 0:X7=0; 1:X2=1234; 1:X7=0;
0:X2=1; 0:X7=0; 1:X2=1234; 1:X7=9;
0:X2=1; 0:X7=9; 1:X2=0; 1:X7=0;
0:X2=1; 0:X7=9; 1:X2=1; 1:X7=0;
0:X2=1; 0:X7=9; 1:X2=1; 1:X7=9;
0:X2=1; 0:X7=9; 1:X2=1234; 1:X7=0;
0:X2=1; 0:X7=9; 1:X2=1234; 1:X7=9;
0:X2=1234; 0:X7=0; 1:X2=0; 1:X7=0;
0:X2=1234; 0:X7=0; 1:X2=1; 1:X7=0;
0:X2=1234; 0:X7=0; 1:X2=1; 1:X7=9;
0:X2=1234; 0:X7=0; 1:X2=1234; 1:X7=0;
0:X2=1234; 0:X7=0; 1:X2=1234; 1:X7=9;
0:X2=1234; 0:X7=9; 1:X2=0; 1:X7=0;
0:X2=1234; 0:X7=9; 1:X2=1; 1:X7=0;
0:X2=1234; 0:X7=9; 1:X2=1; 1:X7=9;
0:X2=1234; 0:X7=9; 1:X2=1234; 1:X7=0;
0:X2=1234; 0:X7=9; 1:X2=1234; 1:X7=9;
No
Witnesses
Positive: 0 Negative: 48
Condition exists (0:X2=0 /\ 0:X7=9 / 1:X2=0 /\ 1:X7=9)
Observation SeqCst Never 0 48
With all the tests we already have, do you think we are good enough to keep the exclusive part of this PR?

-------------

PR: https://git.openjdk.java.net/jdk/pull/2788