RFR: 8360654: AArch64: Remove redundant dmb from C1 compareAndSet

[Samuel Chee]

On Fri, 27 Jun 2025 12:54:07 GMT, Andrew Haley <aph at openjdk.org> wrote:

>> I can double check with the herd7 simulator, but since the `casal` will always produce an acquire, to me it seems impossible that a load can be moved before the `casal` due the acquire within the `casal`. 
>> 
>> Clause 9 of before-barrier-ordering in the Arm Architecture reference manual also supports this.
>
>> Clause 9 of before-barrier-ordering in the Arm Architecture reference manual also supports this.
> 
> Which clause is that?

Hi @theRealAph,

The clause can be find here, the last bullet point on this page - https://mozilla.github.io/pdf.js/web/viewer.html?file=https://documentation-service.arm.com/static/6839d7585475b403d943b4dc#page=255&pagemode=none

Also, we have come up with two herd7 tests which should hopefully prove it to be alright.

{
x=0;
y=0;
0:X1=x; 0:X3=y;
1:X1=x; 1:X3=y;
}
 P0                   | P1             ;
 MOV W0,#1            | MOV W0, #1     ;
 MOV W2,#2            | MOV W2, #2     ;
 CASAL W0, W2, [X1]   | ;
 LDR W4,[X3]          | STR W0, [X3]   ;
                      | DMB ISH        ;
                      | STR W2, [X1]   ;
exists
(0:X0=2 /\ 0:X4=0)


Here, the stores by P1 are happening in order: y = 1; x = 2; and the reads in P0 are happening by CASAL first - from x and then by LDR - from y. The condition constraint checks is that CASAL can't read 2 from x if LDR read 0 from y - the constraint should be fulfilled unless the reads are reordered.

And

{
x = 1; y =1;
0: X1=x; 0:X3=y;
1: X3=x; 1:X1=y;
}

P0                  | P1  ;
MOV W0, #1          | MOV W0, #1;
MOV W2, #2          | MOV W2, #2;
CASAL W0, W2, [X1]  | CASAL W0, W2, [X1];
LDR W4, [X3]        | LDR W4, [X3];

exists
 (0:X4=1 /\ 1: X4=1)
 ```
Here, both X4's being equal to 1 is disallowed, as that would indicate that one of the ldrs was reordered before the CASAL. As the CASAL's will always succeed by default meaning atleast one of the LDR's will load a non-1 value into W4. Hence  (0:X4=1 /\ 1: X4=1) can only ever occur if an ldr gets ordered before the CASAL.

Hope this helps :)

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

PR Comment: https://git.openjdk.org/jdk/pull/26000#issuecomment-3036824254