Sat Jan 13 00:09:10 CET 2024
%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for SB.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 SB
"PodWR Fre PodWR Fre"

{
 0:X1=x; 0:X2=y;
 1:X1=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | MOV W0,#1   ;
 STR W0,[X1] | STR W0,[X1] ;
 LDR W3,[X2] | LDR W3,[X2] ;

exists (0:X3=0 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w2, #1
	str	w2, [x17]
	ldr	w1, [x0]
	;START _litmus_P1
	mov	w2, #1
	str	w2, [x17]
	ldr	w1, [x0]
Test SB Allowed
Histogram (4 states)
24469 *>0:X3=0; 1:X3=0;
9986352:>0:X3=1; 1:X3=0;
9989177:>0:X3=0; 1:X3=1;
2     :>0:X3=1; 1:X3=1;
Ok

Witnesses
Positive: 24469, Negative: 19975531
Condition exists (0:X3=0 /\ 1:X3=0) is validated
Hash=0e1eb22a42a7de6af162a7e5cbb4e4d3
Cycle=Fre PodWR Fre PodWR
Generator=diycross7 (version 7.56+03)
Com=Fr Fr
Orig=PodWR Fre PodWR Fre
Observation SB Sometimes 24469 19975531
Time SB 1.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for SB+dmb.sy+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 SB+dmb.sy+po
"DMB.SYdWR Fre PodWR Fre"

{
 0:X1=x; 0:X2=y;
 1:X1=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | MOV W0,#1   ;
 STR W0,[X1] | STR W0,[X1] ;
 DMB SY      | LDR W3,[X2] ;
 LDR W3,[X2] |             ;

exists (0:X3=0 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w2, #1
	str	w2, [x17]
	dmb	sy
	ldr	w1, [x0]
	;START _litmus_P1
	mov	w2, #1
	str	w2, [x17]
	ldr	w1, [x0]
Test SB+dmb.sy+po Allowed
Histogram (4 states)
7969  *>0:X3=0; 1:X3=0;
9993551:>0:X3=1; 1:X3=0;
9998316:>0:X3=0; 1:X3=1;
164   :>0:X3=1; 1:X3=1;
Ok

Witnesses
Positive: 7969, Negative: 19992031
Condition exists (0:X3=0 /\ 1:X3=0) is validated
Hash=acd016f60ab03ac5b9097f42209cb065
Cycle=Fre PodWR Fre DMB.SYdWR
Generator=diycross7 (version 7.56+03)
Com=Fr Fr
Orig=DMB.SYdWR Fre PodWR Fre
Observation SB+dmb.sy+po Sometimes 7969 19992031
Time SB+dmb.sy+po 1.17
%%%%%%%%%%%%%%%%%%%%%%%%
% Results for R.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 R
"PodWW Coe PodWR Fre"

{
 0:X1=x; 0:X3=y;
 1:X1=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | MOV W0,#2   ;
 STR W0,[X1] | STR W0,[X1] ;
 MOV W2,#1   | LDR W3,[X2] ;
 STR W2,[X3] |             ;

exists ([y]=2 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w0, #1
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	mov	w2, #2
	str	w2, [x17]
	ldr	w1, [x0]
Test R Allowed
Histogram (4 states)
9999866:>1:X3=0; [y]=1;
133   :>1:X3=1; [y]=1;
9976  *>1:X3=0; [y]=2;
9990025:>1:X3=1; [y]=2;
Ok

Witnesses
Positive: 9976, Negative: 19990024
Condition exists ([y]=2 /\ 1:X3=0) is validated
Hash=4aea2c57cbf1dc72c1fbf77b57062773
Cycle=Fre PodWW Coe PodWR
Generator=diycross7 (version 7.56+03)
Com=Co Fr
Orig=PodWW Coe PodWR Fre
Observation R Sometimes 9976 19990024
Time R 0.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for R+dmb.sy+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 R+dmb.sy+po
"DMB.SYdWW Coe PodWR Fre"

{
 0:X1=x; 0:X3=y;
 1:X1=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | MOV W0,#2   ;
 STR W0,[X1] | STR W0,[X1] ;
 DMB SY      | LDR W3,[X2] ;
 MOV W2,#1   |             ;
 STR W2,[X3] |             ;

exists ([y]=2 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w0, #1
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	mov	w2, #2
	str	w2, [x17]
	ldr	w1, [x0]
Test R+dmb.sy+po Allowed
Histogram (4 states)
10001649:>1:X3=0; [y]=1;
290   :>1:X3=1; [y]=1;
162   *>1:X3=0; [y]=2;
9997899:>1:X3=1; [y]=2;
Ok

Witnesses
Positive: 162, Negative: 19999838
Condition exists ([y]=2 /\ 1:X3=0) is validated
Hash=0e843011df9fd5cccf3979cd65b81870
Cycle=Fre DMB.SYdWW Coe PodWR
Generator=diycross7 (version 7.56+03)
Com=Co Fr
Orig=DMB.SYdWW Coe PodWR Fre
Observation R+dmb.sy+po Sometimes 162 19999838
Time R+dmb.sy+po 1.19
%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for MP.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 MP
"PodWW Rfe PodRR Fre"

{
 0:X1=x; 0:X3=y;
 1:X0=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W1,[X0] ;
 STR W0,[X1] | LDR W3,[X2] ;
 MOV W2,#1   |             ;
 STR W2,[X3] |             ;

exists (1:X1=1 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w0, #1
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	ldr	w3, [x0]
	ldr	w2, [x1]
Test MP Allowed
Histogram (4 states)
10005589:>1:X1=0; 1:X3=0;
3498  *>1:X1=1; 1:X3=0;
4429  :>1:X1=0; 1:X3=1;
9986484:>1:X1=1; 1:X3=1;
Ok

Witnesses
Positive: 3498, Negative: 19996502
Condition exists (1:X1=1 /\ 1:X3=0) is validated
Hash=9827c55a473553b4e097483de0205966
Cycle=Rfe PodRR Fre PodWW
Generator=diycross7 (version 7.56+03)
Com=Rf Fr
Orig=PodWW Rfe PodRR Fre
Observation MP Sometimes 3498 19996502
Time MP 0.92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for MP+dmb.sy+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 MP+dmb.sy+po
"DMB.SYdWW Rfe PodRR Fre"

{
 0:X1=x; 0:X3=y;
 1:X0=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W1,[X0] ;
 STR W0,[X1] | LDR W3,[X2] ;
 DMB SY      |             ;
 MOV W2,#1   |             ;
 STR W2,[X3] |             ;

exists (1:X1=1 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w0, #1
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	ldr	w3, [x0]
	ldr	w2, [x1]
Test MP+dmb.sy+po Allowed
Histogram (3 states)
10001500:>1:X1=0; 1:X3=0;
3679  :>1:X1=0; 1:X3=1;
9994821:>1:X1=1; 1:X3=1;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists (1:X1=1 /\ 1:X3=0) is NOT validated
Hash=4e133de79065843db2e2bbaf079d080a
Cycle=Rfe PodRR Fre DMB.SYdWW
Generator=diycross7 (version 7.56+03)
Com=Rf Fr
Orig=DMB.SYdWW Rfe PodRR Fre
Observation MP+dmb.sy+po Never 0 20000000
Time MP+dmb.sy+po 1.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for SB+dmb.sys.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 SB+dmb.sys
"DMB.SYdWR Fre DMB.SYdWR Fre"

{
 0:X1=x; 0:X2=y;
 1:X1=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | MOV W0,#1   ;
 STR W0,[X1] | STR W0,[X1] ;
 DMB SY      | DMB SY      ;
 LDR W3,[X2] | LDR W3,[X2] ;

exists (0:X3=0 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w2, #1
	str	w2, [x17]
	dmb	sy
	ldr	w1, [x0]
	;START _litmus_P1
	mov	w2, #1
	str	w2, [x17]
	dmb	sy
	ldr	w1, [x0]
Test SB+dmb.sys Allowed
Histogram (3 states)
10000270:>0:X3=1; 1:X3=0;
9999172:>0:X3=0; 1:X3=1;
558   :>0:X3=1; 1:X3=1;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:X3=0 /\ 1:X3=0) is NOT validated
Hash=c6a533fb255005c1a89998321e552a86
Cycle=Fre DMB.SYdWR Fre DMB.SYdWR
Generator=diycross7 (version 7.56+03)
Com=Fr Fr
Orig=DMB.SYdWR Fre DMB.SYdWR Fre
Observation SB+dmb.sys Never 0 20000000
Time SB+dmb.sys 1.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for R+po+dmb.sy.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 R+po+dmb.sy
"PodWW Coe DMB.SYdWR Fre"

{
 0:X1=x; 0:X3=y;
 1:X1=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | MOV W0,#2   ;
 STR W0,[X1] | STR W0,[X1] ;
 MOV W2,#1   | DMB SY      ;
 STR W2,[X3] | LDR W3,[X2] ;

exists ([y]=2 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w0, #1
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	mov	w2, #2
	str	w2, [x17]
	dmb	sy
	ldr	w1, [x0]
Test R+po+dmb.sy Allowed
Histogram (4 states)
9999764:>1:X3=0; [y]=1;
369   :>1:X3=1; [y]=1;
8874  *>1:X3=0; [y]=2;
9990993:>1:X3=1; [y]=2;
Ok

Witnesses
Positive: 8874, Negative: 19991126
Condition exists ([y]=2 /\ 1:X3=0) is validated
Hash=f8a6aa6da9a958eb179dcab604d3a51e
Cycle=Fre PodWW Coe DMB.SYdWR
Generator=diycross7 (version 7.56+03)
Com=Co Fr
Orig=PodWW Coe DMB.SYdWR Fre
Observation R+po+dmb.sy Sometimes 8874 19991126
Time R+po+dmb.sy 1.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for R+dmb.sys.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 R+dmb.sys
"DMB.SYdWW Coe DMB.SYdWR Fre"

{
 0:X1=x; 0:X3=y;
 1:X1=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | MOV W0,#2   ;
 STR W0,[X1] | STR W0,[X1] ;
 DMB SY      | DMB SY      ;
 MOV W2,#1   | LDR W3,[X2] ;
 STR W2,[X3] |             ;

exists ([y]=2 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w0, #1
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	mov	w2, #2
	str	w2, [x17]
	dmb	sy
	ldr	w1, [x0]
Test R+dmb.sys Allowed
Histogram (3 states)
10001145:>1:X3=0; [y]=1;
763   :>1:X3=1; [y]=1;
9998092:>1:X3=1; [y]=2;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists ([y]=2 /\ 1:X3=0) is NOT validated
Hash=d8feed7146fa9f77ff983d26efc9d029
Cycle=Fre DMB.SYdWW Coe DMB.SYdWR
Generator=diycross7 (version 7.56+03)
Com=Co Fr
Orig=DMB.SYdWW Coe DMB.SYdWR Fre
Observation R+dmb.sys Never 0 20000000
Time R+dmb.sys 1.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for MP+po+dmb.sy.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 MP+po+dmb.sy
"PodWW Rfe DMB.SYdRR Fre"

{
 0:X1=x; 0:X3=y;
 1:X0=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W1,[X0] ;
 STR W0,[X1] | DMB SY      ;
 MOV W2,#1   | LDR W3,[X2] ;
 STR W2,[X3] |             ;

exists (1:X1=1 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w0, #1
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	ldr	w3, [x0]
	dmb	sy
	ldr	w2, [x1]
Test MP+po+dmb.sy Allowed
Histogram (4 states)
10005434:>1:X1=0; 1:X3=0;
3542  *>1:X1=1; 1:X3=0;
3792  :>1:X1=0; 1:X3=1;
9987232:>1:X1=1; 1:X3=1;
Ok

Witnesses
Positive: 3542, Negative: 19996458
Condition exists (1:X1=1 /\ 1:X3=0) is validated
Hash=5dccf49d050a0fcb3c6ad3f3d8e2a20c
Cycle=Rfe DMB.SYdRR Fre PodWW
Generator=diycross7 (version 7.56+03)
Com=Rf Fr
Orig=PodWW Rfe DMB.SYdRR Fre
Observation MP+po+dmb.sy Sometimes 3542 19996458
Time MP+po+dmb.sy 1.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for MP+dmb.sys.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 MP+dmb.sys
"DMB.SYdWW Rfe DMB.SYdRR Fre"

{
 0:X1=x; 0:X3=y;
 1:X0=y; 1:X2=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W1,[X0] ;
 STR W0,[X1] | DMB SY      ;
 DMB SY      | LDR W3,[X2] ;
 MOV W2,#1   |             ;
 STR W2,[X3] |             ;

exists (1:X1=1 /\ 1:X3=0)
Generated assembler
	;START _litmus_P0
	mov	w0, #1
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	ldr	w3, [x0]
	dmb	sy
	ldr	w2, [x1]
Test MP+dmb.sys Allowed
Histogram (3 states)
10002632:>1:X1=0; 1:X3=0;
5853  :>1:X1=0; 1:X3=1;
9991515:>1:X1=1; 1:X3=1;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists (1:X1=1 /\ 1:X3=0) is NOT validated
Hash=ba6fa85f3a14d91cf1d52c22f60d9b83
Cycle=Rfe DMB.SYdRR Fre DMB.SYdWW
Generator=diycross7 (version 7.56+03)
Com=Rf Fr
Orig=DMB.SYdWW Rfe DMB.SYdRR Fre
Observation MP+dmb.sys Never 0 20000000
Time MP+dmb.sys 1.33
%%%%%%%%%%%%%%%%%%%%%%%%
% Results for S.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 S
"PodWW Rfe PodRW Coe"

{
 0:X1=x; 0:X3=y;
 1:X0=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#2   | LDR W1,[X0] ;
 STR W0,[X1] | MOV W2,#1   ;
 MOV W2,#1   | STR W2,[X3] ;
 STR W2,[X3] |             ;

exists ([x]=2 /\ 1:X1=1)
Generated assembler
	;START _litmus_P0
	mov	w0, #2
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	ldr	w1, [x17]
	mov	w2, #1
	str	w2, [x0]
Test S Allowed
Histogram (4 states)
11779 :>1:X1=0; [x]=1;
9988538:>1:X1=1; [x]=1;
9999440:>1:X1=0; [x]=2;
243   *>1:X1=1; [x]=2;
Ok

Witnesses
Positive: 243, Negative: 19999757
Condition exists ([x]=2 /\ 1:X1=1) is validated
Hash=4a8390a6db1dd4bb80b5f2347e861742
Cycle=Rfe PodRW Coe PodWW
Generator=diycross7 (version 7.56+03)
Com=Rf Co
Orig=PodWW Rfe PodRW Coe
Observation S Sometimes 243 19999757
Time S 0.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for S+po+dmb.sy.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 S+po+dmb.sy
"PodWW Rfe DMB.SYdRW Coe"

{
 0:X1=x; 0:X3=y;
 1:X0=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#2   | LDR W1,[X0] ;
 STR W0,[X1] | DMB SY      ;
 MOV W2,#1   | MOV W2,#1   ;
 STR W2,[X3] | STR W2,[X3] ;

exists ([x]=2 /\ 1:X1=1)
Generated assembler
	;START _litmus_P0
	mov	w0, #2
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	ldr	w1, [x17]
	dmb	sy
	mov	w2, #1
	str	w2, [x0]
Test S+po+dmb.sy Allowed
Histogram (4 states)
11985 :>1:X1=0; [x]=1;
9988349:>1:X1=1; [x]=1;
9999588:>1:X1=0; [x]=2;
78    *>1:X1=1; [x]=2;
Ok

Witnesses
Positive: 78, Negative: 19999922
Condition exists ([x]=2 /\ 1:X1=1) is validated
Hash=7bdbb892d7eecca9087d4ce0dfb0f475
Cycle=Rfe DMB.SYdRW Coe PodWW
Generator=diycross7 (version 7.56+03)
Com=Rf Co
Orig=PodWW Rfe DMB.SYdRW Coe
Observation S+po+dmb.sy Sometimes 78 19999922
Time S+po+dmb.sy 1.11
%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for LB.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 LB
"PodRW Rfe PodRW Rfe"

{
 0:X0=x; 0:X3=y;
 1:X0=y; 1:X3=x;
}
 P0          | P1          ;
 LDR W1,[X0] | LDR W1,[X0] ;
 MOV W2,#1   | MOV W2,#1   ;
 STR W2,[X3] | STR W2,[X3] ;

exists (0:X1=1 /\ 1:X1=1)
Generated assembler
	;START _litmus_P0
	ldr	w1, [x17]
	mov	w2, #1
	str	w2, [x0]
	;START _litmus_P1
	ldr	w1, [x17]
	mov	w2, #1
	str	w2, [x0]
Test LB Allowed
Histogram (3 states)
18262 :>0:X1=0; 1:X1=0;
9992834:>0:X1=1; 1:X1=0;
9988904:>0:X1=0; 1:X1=1;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:X1=1 /\ 1:X1=1) is NOT validated
Hash=75efc9d3fd2408a0f1d61e2dbe4a5037
Cycle=Rfe PodRW Rfe PodRW
Generator=diycross7 (version 7.56+03)
Com=Rf Rf
Orig=PodRW Rfe PodRW Rfe
Observation LB Never 0 20000000
Time LB 0.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for LB+dmb.sy+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 LB+dmb.sy+po
"DMB.SYdRW Rfe PodRW Rfe"

{
 0:X0=x; 0:X3=y;
 1:X0=y; 1:X3=x;
}
 P0          | P1          ;
 LDR W1,[X0] | LDR W1,[X0] ;
 DMB SY      | MOV W2,#1   ;
 MOV W2,#1   | STR W2,[X3] ;
 STR W2,[X3] |             ;

exists (0:X1=1 /\ 1:X1=1)
Generated assembler
	;START _litmus_P0
	ldr	w1, [x17]
	dmb	sy
	mov	w2, #1
	str	w2, [x0]
	;START _litmus_P1
	ldr	w1, [x17]
	mov	w2, #1
	str	w2, [x0]
Test LB+dmb.sy+po Allowed
Histogram (3 states)
12790 :>0:X1=0; 1:X1=0;
9992194:>0:X1=1; 1:X1=0;
9995016:>0:X1=0; 1:X1=1;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:X1=1 /\ 1:X1=1) is NOT validated
Hash=8083d9ae4ef74f218457001062189689
Cycle=Rfe PodRW Rfe DMB.SYdRW
Generator=diycross7 (version 7.56+03)
Com=Rf Rf
Orig=DMB.SYdRW Rfe PodRW Rfe
Observation LB+dmb.sy+po Never 0 20000000
Time LB+dmb.sy+po 1.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for S+dmb.sy+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 S+dmb.sy+po
"DMB.SYdWW Rfe PodRW Coe"

{
 0:X1=x; 0:X3=y;
 1:X0=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#2   | LDR W1,[X0] ;
 STR W0,[X1] | MOV W2,#1   ;
 DMB SY      | STR W2,[X3] ;
 MOV W2,#1   |             ;
 STR W2,[X3] |             ;

exists ([x]=2 /\ 1:X1=1)
Generated assembler
	;START _litmus_P0
	mov	w0, #2
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	ldr	w1, [x17]
	mov	w2, #1
	str	w2, [x0]
Test S+dmb.sy+po Allowed
Histogram (3 states)
10386 :>1:X1=0; [x]=1;
9989614:>1:X1=1; [x]=1;
10000000:>1:X1=0; [x]=2;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists ([x]=2 /\ 1:X1=1) is NOT validated
Hash=15ad98e55f7098898ad567e00f3adb87
Cycle=Rfe PodRW Coe DMB.SYdWW
Generator=diycross7 (version 7.56+03)
Com=Rf Co
Orig=DMB.SYdWW Rfe PodRW Coe
Observation S+dmb.sy+po Never 0 20000000
Time S+dmb.sy+po 1.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for S+dmb.sys.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 S+dmb.sys
"DMB.SYdWW Rfe DMB.SYdRW Coe"

{
 0:X1=x; 0:X3=y;
 1:X0=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#2   | LDR W1,[X0] ;
 STR W0,[X1] | DMB SY      ;
 DMB SY      | MOV W2,#1   ;
 MOV W2,#1   | STR W2,[X3] ;
 STR W2,[X3] |             ;

exists ([x]=2 /\ 1:X1=1)
Generated assembler
	;START _litmus_P0
	mov	w0, #2
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	ldr	w1, [x17]
	dmb	sy
	mov	w2, #1
	str	w2, [x0]
Test S+dmb.sys Allowed
Histogram (3 states)
10583 :>1:X1=0; [x]=1;
9989746:>1:X1=1; [x]=1;
9999671:>1:X1=0; [x]=2;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists ([x]=2 /\ 1:X1=1) is NOT validated
Hash=2a684d141e99d8a17d8801bd6311d477
Cycle=Rfe DMB.SYdRW Coe DMB.SYdWW
Generator=diycross7 (version 7.56+03)
Com=Rf Co
Orig=DMB.SYdWW Rfe DMB.SYdRW Coe
Observation S+dmb.sys Never 0 20000000
Time S+dmb.sys 1.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for LB+dmb.sys.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 LB+dmb.sys
"DMB.SYdRW Rfe DMB.SYdRW Rfe"

{
 0:X0=x; 0:X3=y;
 1:X0=y; 1:X3=x;
}
 P0          | P1          ;
 LDR W1,[X0] | LDR W1,[X0] ;
 DMB SY      | DMB SY      ;
 MOV W2,#1   | MOV W2,#1   ;
 STR W2,[X3] | STR W2,[X3] ;

exists (0:X1=1 /\ 1:X1=1)
Generated assembler
	;START _litmus_P0
	ldr	w1, [x17]
	dmb	sy
	mov	w2, #1
	str	w2, [x0]
	;START _litmus_P1
	ldr	w1, [x17]
	dmb	sy
	mov	w2, #1
	str	w2, [x0]
Test LB+dmb.sys Allowed
Histogram (3 states)
12418 :>0:X1=0; 1:X1=0;
9993770:>0:X1=1; 1:X1=0;
9993812:>0:X1=0; 1:X1=1;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists (0:X1=1 /\ 1:X1=1) is NOT validated
Hash=58f58841a29b4785c0318afb13b06b93
Cycle=Rfe DMB.SYdRW Rfe DMB.SYdRW
Generator=diycross7 (version 7.56+03)
Com=Rf Rf
Orig=DMB.SYdRW Rfe DMB.SYdRW Rfe
Observation LB+dmb.sys Never 0 20000000
Time LB+dmb.sys 1.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for 2+2W.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 2+2W
"PodWW Coe PodWW Coe"

{
 0:X1=x; 0:X3=y;
 1:X1=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#2   | MOV W0,#2   ;
 STR W0,[X1] | STR W0,[X1] ;
 MOV W2,#1   | MOV W2,#1   ;
 STR W2,[X3] | STR W2,[X3] ;

exists ([x]=2 /\ [y]=2)
Generated assembler
	;START _litmus_P0
	mov	w0, #2
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	mov	w0, #2
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
Test 2+2W Allowed
Histogram (4 states)
1038  :>[x]=1; [y]=1;
9999132:>[x]=2; [y]=1;
9998998:>[x]=1; [y]=2;
832   *>[x]=2; [y]=2;
Ok

Witnesses
Positive: 832, Negative: 19999168
Condition exists ([x]=2 /\ [y]=2) is validated
Hash=5112e7c862483914f9d4e140b60657b2
Cycle=Coe PodWW Coe PodWW
Generator=diycross7 (version 7.56+03)
Com=Co Co
Orig=PodWW Coe PodWW Coe
Observation 2+2W Sometimes 832 19999168
Time 2+2W 0.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for 2+2W+dmb.sy+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 2+2W+dmb.sy+po
"DMB.SYdWW Coe PodWW Coe"

{
 0:X1=x; 0:X3=y;
 1:X1=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#2   | MOV W0,#2   ;
 STR W0,[X1] | STR W0,[X1] ;
 DMB SY      | MOV W2,#1   ;
 MOV W2,#1   | STR W2,[X3] ;
 STR W2,[X3] |             ;

exists ([x]=2 /\ [y]=2)
Generated assembler
	;START _litmus_P0
	mov	w0, #2
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	mov	w0, #2
	str	w0, [x16]
	mov	w17, #1
	str	w17, [x15]
Test 2+2W+dmb.sy+po Allowed
Histogram (4 states)
678   :>[x]=1; [y]=1;
9999717:>[x]=2; [y]=1;
9999322:>[x]=1; [y]=2;
283   *>[x]=2; [y]=2;
Ok

Witnesses
Positive: 283, Negative: 19999717
Condition exists ([x]=2 /\ [y]=2) is validated
Hash=5dbeaed3a1aa88c4cdded063346ba075
Cycle=Coe PodWW Coe DMB.SYdWW
Generator=diycross7 (version 7.56+03)
Com=Co Co
Orig=DMB.SYdWW Coe PodWW Coe
Observation 2+2W+dmb.sy+po Sometimes 283 19999717
Time 2+2W+dmb.sy+po 1.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for 2+2W+dmb.sys.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
AArch64 2+2W+dmb.sys
"DMB.SYdWW Coe DMB.SYdWW Coe"

{
 0:X1=x; 0:X3=y;
 1:X1=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#2   | MOV W0,#2   ;
 STR W0,[X1] | STR W0,[X1] ;
 DMB SY      | DMB SY      ;
 MOV W2,#1   | MOV W2,#1   ;
 STR W2,[X3] | STR W2,[X3] ;

exists ([x]=2 /\ [y]=2)
Generated assembler
	;START _litmus_P0
	mov	w0, #2
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
	;START _litmus_P1
	mov	w0, #2
	str	w0, [x16]
	dmb	sy
	mov	w17, #1
	str	w17, [x15]
Test 2+2W+dmb.sys Allowed
Histogram (3 states)
808   :>[x]=1; [y]=1;
9999676:>[x]=2; [y]=1;
9999516:>[x]=1; [y]=2;
No

Witnesses
Positive: 0, Negative: 20000000
Condition exists ([x]=2 /\ [y]=2) is NOT validated
Hash=9495f1f810a4f034c732242a8a2c3eed
Cycle=Coe DMB.SYdWW Coe DMB.SYdWW
Generator=diycross7 (version 7.56+03)
Com=Co Co
Orig=DMB.SYdWW Coe DMB.SYdWW Coe
Observation 2+2W+dmb.sys Never 0 20000000
Time 2+2W+dmb.sys 1.35
Revision 888fccb005fdadf81d11eea5df99d5c3c366984e, version 7.56+03
Command line: litmus7 -mach M1 -a 4 -o R @all
Parameters
#define SIZE_OF_TEST 5000
#define NUMBER_OF_RUN 2000
#define AVAIL 4
#define STRIDE 1
#define MAX_LOOP 0
/* gcc options: -Wall -std=gnu99 -O2 */
/* barrier: user */
/* launch: changing */
/* affinity: none */
/* memory: direct */
/* stride: 1 */
/* safer: write */
/* preload: random */
/* speedcheck: no */
/* alloc: dynamic */
/* proc used: 4 */
GCC=gcc
LITMUSOPTS=
Sat Jan 13 00:09:39 CET 2024