Zero registers, memory orderings and dependencies

[hernanponcedeleon]

I am trying to understand how zero registers (e.g., WZR in aarch64) interact with the memory orderings and data/addr/ctrl dependencies.

Consider this variation on MP+ctrl with rel-acq semantics

AArch64 MP+ctrl
{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x; 1:X5=z;
x=1; y=1;
}
 P0           | P1            ;
 MOV W0,#0    | LDAR WZR,[X1] ;
 STR W0,[X1]  | CBNZ WZR,LC00 ;
 MOV W2,#0    | LC00:         ;
 STLR W2,[X3] | LDR W2,[X3]   ;
exists
(1:XZR=0 /\ 1:X2=1)

where the values 0/1 are reverted wrt the usual MP, and the first load targets the zero register.

The exists is satisfiable despite the rel-acq because the acq-load can execute first, obtain value 1 and then "override" the target register with value zero.

The fact that the only witness graph having W2=1 has an event c: R[y]Acq=1 makes me believe that the acquire semantics are preserved and herd internally then create some local event WRZ <- 0. However, I could not see such local event even if I added showevents all.

Adding option doshow ctrl does not show a ctrl edge from the first to the second load (which I have if I replace WZR by W0). This again suggest the existence of the local event I mentioned above.

Am I right that P1 is internally modeled as follows?

DUMMY = R[y]_Acq
WZR <- 0
if WZR != 0 goto LC00
LC00
W2= R[x]

meaning loads targeting zero registers preserve their memory order, but they are not in the domain of the data,addr,ctrl relations.

[maranget]

Hi @hernanponcedeleon. The result is not surprising as the value of the XZR "register" is always zero. Said otherwise, You just cannot write into it. Hence the pseudo-code would rather be:

DUMMY = R[y]_Acq
if WZR != 0 goto LC00
LC00
W2= R[x]

Hence I guess there should be no control dependency!

Also consider there there is no architectural way to check the value read by the LDAR instruction of P1. Hence if P1 executes "before" P0 1:X2 final value is 1 if P1 executes "after" P0 the final value of 1:X2 is zero. In all cases, whatever occurred, the final value of 1:XZR is zero.

Notice that litmus is wrong here, as it lets gcc reallocate "XZR" to an ordinary register, resulting in a potential final value of 1. Thank you for discovering this (litmus) bug.

[hernanponcedeleon]

Hi @hernanponcedeleon. The result is not surprising as the value of the XZR "register" is always zero. Said otherwise, You just cannot write into it.

Arm's documentations is not so clear about this, it claims "The zero registers, XZR and WZR, always read as 0 and ignore writes." which I find it different that "you cannot write to those registers".

Hence the pseudo-code would rather be:

DUMMY = R[y]_Acq
if WZR != 0 goto LC00
LC00
W2= R[x]

Just to be sure, is it valid to use zero registers as targets of loads and it is herd's responsibility to do the transformation above?

Hence I guess there should be no control dependency!

Assuming the psuedo-code is the intended architectural behavior, I agree.
This clarifies my main question.

Also consider there there is no architectural way to check the value read by the LDAR instruction of P1. Hence if P1 executes "before" P0 1:X2 final value is 1 if P1 executes "after" P0 the final value of 1:X2 is zero. In all cases, whatever occurred, the final value of 1:XZR is zero.

Notice that litmus is wrong here, as it lets gcc reallocate "XZR" to an ordinary register, resulting in a potential final value of 1. Thank you for discovering this (litmus) bug.

Nice side effect :D