AArch64 C11-Z-forbid (* Another test by Skaked. Consider this C11 forbidden execution: ,-> a:Wsc x=2 ,-> d:Rsc x=4 ,-- f:Wrlx y=1 | b:Wrlx x=3 / e:Rsc y=1 <-rf-' g:Wsc y=2 | c:Wrlx x=4 -rf-' h:Wsc x=1 | | '--------------------------co------------------' mapped to AArch64: ,-> a:Wrel x=2 ,-> d:Racq x=4 ,-- f:W y=1 | b:W x=3 / e:Racq y=1 <-rf-' g:Wrel y=2 | c:W x=4 -rf-' h:Wrel x=1 | | '--------------------------co-------------------' We use the satisfied load-acquire token to forbid this execution. But at the same time we want a similar execution that differs only by the co-order of x, 2;1;3;4, to be allowed as it is allowed by C11. *) Hash=0fb12520c15fe9630a02aff3ff997061 { 0:X1=x; 1:X1=x; 1:X3=y; 2:X1=x; 2:X3=y; } P0 | P1 | P2 ; MOV W0,#2 | LDAR W2,[X1] | MOV W0,#1 ; STLR W0,[X1] | LDAR W4,[X3] | STR W0,[X3] ; MOV W3,#3 | | MOV W2,#2 ; STR W3,[X1] | | STLR W2,[X3]; MOV W4,#4 | | MOV W5,#1 ; STR W4,[X1] | | STLR W5,[X1]; | | LDR W4,[X1] ; Observed y=2; x=4; 2:X4=4; 1:X4=1; 1:X2=3;