Wed Dec 23 16:27:33 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww000
"DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 ;
li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | ;
exists (x=2 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww000 Allowed
Histogram (3 states)
80224197:>1:r1=0; x=1;
247193614:>1:r1=1; x=1;
312582189:>1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=262d40103ab036ada7c4d5ede4cb5840
Cycle=DpdW Wse SyncdWW Rfe
Relax bcsdww000 No BCSyncdWW
Safe=Wse DpdW
Time bcsdww000 81.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww001
"DpdW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 | sync | li r4,1 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: xor 31,3,3
_litmus_P3_2_: li 10,1
_litmus_P3_3_: stwx 10,31,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww001 Allowed
Histogram (15 states)
610060:>1:r1=1; 3:r1=1; x=2; z=1;
626370:>1:r1=1; 3:r1=1; x=1; z=2;
1532519:>1:r1=1; 3:r1=0; x=2; z=2;
1254893:>1:r1=0; 3:r1=1; x=2; z=2;
16364395:>1:r1=1; 3:r1=0; x=2; z=1;
15993026:>1:r1=1; 3:r1=0; x=1; z=2;
13807730:>1:r1=0; 3:r1=1; x=2; z=1;
3119255:>1:r1=0; 3:r1=0; x=1; z=1;
42499903:>1:r1=0; 3:r1=0; x=1; z=2;
44933966:>1:r1=0; 3:r1=0; x=2; z=1;
35323206:>1:r1=1; 3:r1=0; x=1; z=1;
32435888:>1:r1=0; 3:r1=1; x=1; z=1;
70435213:>1:r1=0; 3:r1=0; x=2; z=2;
27434089:>1:r1=1; 3:r1=1; x=1; z=1;
13629487:>1:r1=0; 3:r1=1; x=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=96b3ad5ef3552835e91cfb053b388e47
Cycle=DpdW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww001 No BCSyncdWW
Safe=Wse DpdW
Time bcsdww001 91.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww002
"SyncdRW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | li r4,1 | sync | li r3,1 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: li 4,1
_litmus_P3_3_: stw 4,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww002 Allowed
Histogram (15 states)
728819:>1:r1=1; 3:r1=1; x=1; z=2;
17443244:>1:r1=1; 3:r1=0; x=1; z=2;
5673243:>1:r1=0; 3:r1=0; x=1; z=1;
1137572:>1:r1=1; 3:r1=0; x=2; z=2;
637264:>1:r1=0; 3:r1=1; x=2; z=2;
24529130:>1:r1=1; 3:r1=1; x=1; z=1;
48271725:>1:r1=0; 3:r1=0; x=1; z=2;
8824056:>1:r1=0; 3:r1=1; x=2; z=1;
46995859:>1:r1=0; 3:r1=0; x=2; z=1;
12765850:>1:r1=0; 3:r1=1; x=1; z=2;
32189219:>1:r1=0; 3:r1=1; x=1; z=1;
64575678:>1:r1=0; 3:r1=0; x=2; z=2;
13980878:>1:r1=1; 3:r1=0; x=2; z=1;
41996052:>1:r1=1; 3:r1=0; x=1; z=1;
251411:>1:r1=1; 3:r1=1; x=2; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=af33a9d4f6f79386d356cbbdb0662698
Cycle=SyncdRW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww002 No BCSyncdWW
Safe=Wse SyncdRW DpdW
Time bcsdww002 88.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww003
"DpdR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 | sync | lwzx r4,r3,r5 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 10,30,30
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww003 Allowed
Histogram (15 states)
2128488:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
1028143:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
863076:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
1896826:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
43061198:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
14301029:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
30613140:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
19074710:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
72821135:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
27866850:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
41167416:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
33613661:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
13699715:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
732715:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
17131898:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=6c72af0e6695d87de072985a4977a496
Cycle=DpdR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww003 No BCSyncdWW
Safe=Fre Wse DpdW DpdR
Time bcsdww003 92.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww004
"DpsR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 | sync | lwzx r4,r3,r2 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: xor 10,4,4
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 31,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,31,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww004 Allowed
Histogram (42 states)
10 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
2747 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
10607 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
14804 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
19021 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
58790 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
5003 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
4910 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
30482 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
212953:>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
13348 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
134978:>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
37499 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
32515 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
132583:>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
119726:>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
67826 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
970786:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
1092377:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
27139 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
339791:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
534943:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
563765:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
10183725:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
2097586:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
59349 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
7349468:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
4391525:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
12014699:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
33347852:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
3755577:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
1763330:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
13149789:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
21706829:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
25767528:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
38966856:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
4215777:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
25719193:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
9106206:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
26197289:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
17893436:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
57887383:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=26d413fc2e2cdadfa9e0f1aeb3ab365b
Cycle=DpsR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww004 No BCSyncdWW
Safe=Fre Wse DpsR DpdW
Time bcsdww004 93.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww005
"SyncdRR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | li r4,1 | sync | lwz r3,0(r4) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww005 Allowed
Histogram (15 states)
646964:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1066474:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
4014424:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
1227659:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
44140692:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
32304468:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
45706869:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
35477554:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
68568950:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
14541657:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
14940362:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
26333841:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
14988046:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
779755:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
15262285:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=9d8e29c8c4e565bae4fdb78aec0db9b5
Cycle=SyncdRR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww005 No BCSyncdWW
Safe=Fre Wse SyncdRR DpdW
Time bcsdww005 94.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww006
"SyncsRR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | li r4,1 | sync | lwz r3,0(r2) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 31,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,31,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww006 Allowed
Histogram (42 states)
844 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
302116:>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
524633:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
1653498:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
501440:>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
281786:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
151947:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
311534:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
1381665:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
1447738:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
909260:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
489475:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
396632:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
539086:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
3231529:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
2634959:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
140612:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
2896961:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
7086465:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
3863610:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
1813292:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
3254515:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
372938:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
672859:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
15462980:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
12637364:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
477319:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1714909:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
1668191:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
1918253:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
24058933:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
8127997:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
11611171:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
8935384:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
6191189:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
8904834:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
19950556:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
34888921:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
53579940:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
24476329:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
20986425:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
29549911:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=62faf55c9e7916888e6ae088e9375bff
Cycle=SyncsRR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww006 No BCSyncdWW
Safe=Fre Wse SyncsRR DpdW
Time bcsdww006 94.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww007
"DpdW Wse SyncdWW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | li r4,1 ;
li r3,1 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww007 Allowed
Histogram (7 states)
15768282:>2:r1=1; x=1; y=2;
35556691:>2:r1=0; x=2; y=2;
23004601:>2:r1=1; x=2; y=1;
8524363:>2:r1=0; x=1; y=1;
121145479:>2:r1=0; x=2; y=1;
92808156:>2:r1=1; x=1; y=1;
103192428:>2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=7c2462ff041c713f8de949f757a40d53
Cycle=DpdW Wse SyncdWW Wse SyncdWW Rfe
Relax bcsdww007 No BCSyncdWW
Safe=Wse SyncdWW DpdW
Time bcsdww007 74.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww008
"SyncdRW Wse SyncdWW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | li r3,1 ;
li r3,1 | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww008 Allowed
Histogram (7 states)
27612867:>2:r1=0; x=2; y=2;
16913032:>2:r1=0; x=1; y=1;
13037668:>2:r1=1; x=2; y=1;
115486158:>2:r1=0; x=1; y=2;
127604028:>2:r1=0; x=2; y=1;
88441852:>2:r1=1; x=1; y=1;
10904395:>2:r1=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=e6b1c1a0023ee13d1ea18feb286c6d13
Cycle=SyncdRW Wse SyncdWW Wse SyncdWW Rfe
Relax bcsdww008 No BCSyncdWW
Safe=Wse SyncdWW SyncdRW
Time bcsdww008 75.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww009
"DpdR Fre SyncdWW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r5 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ 2:r1=1 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww009 Allowed
Histogram (7 states)
10991434:>2:r1=0; 2:r4=1; y=1;
8838854:>2:r1=1; 2:r4=1; y=2;
35874851:>2:r1=0; 2:r4=0; y=2;
15617935:>2:r1=1; 2:r4=0; y=1;
140497398:>2:r1=0; 2:r4=0; y=1;
80485295:>2:r1=1; 2:r4=1; y=1;
107694233:>2:r1=0; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=9d7f07ce6da224ac7eca2af4a5915a72
Cycle=DpdR Fre SyncdWW Wse SyncdWW Rfe
Relax bcsdww009 No BCSyncdWW
Safe=Fre Wse SyncdWW DpdR
Time bcsdww009 75.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww010
"DpsR Fre SyncdWW Wse SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r2 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 11,10,9
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww010 Allowed
Histogram (18 states)
594 :>2:r1=0; 2:r4=1; x=2; y=1;
376805:>2:r1=2; 2:r4=1; x=2; y=1;
9182 :>2:r1=2; 2:r4=1; x=1; y=1;
39852 :>2:r1=0; 2:r4=2; x=2; y=1;
331216:>2:r1=0; 2:r4=2; x=1; y=2;
105767:>2:r1=0; 2:r4=1; x=1; y=1;
19843 :>2:r1=1; 2:r4=2; x=1; y=2;
868943:>2:r1=0; 2:r4=1; x=1; y=2;
63508 :>2:r1=0; 2:r4=2; x=1; y=1;
47288538:>2:r1=2; 2:r4=2; x=1; y=2;
58255256:>2:r1=0; 2:r4=0; x=1; y=1;
14596697:>2:r1=1; 2:r4=1; x=2; y=1;
41335732:>2:r1=1; 2:r4=1; x=1; y=2;
98667557:>2:r1=2; 2:r4=2; x=2; y=1;
5128916:>2:r1=2; 2:r4=2; x=1; y=1;
36661756:>2:r1=0; 2:r4=0; x=2; y=1;
28155163:>2:r1=1; 2:r4=1; x=1; y=1;
68094675:>2:r1=0; 2:r4=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=3bd35505ff4c5dbff1bb92ff33d7496b
Cycle=DpsR Fre SyncdWW Wse SyncdWW Rfe
Relax bcsdww010 No BCSyncdWW
Safe=Fre Wse SyncdWW DpsR
Time bcsdww010 74.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww011
"SyncdRR Fre SyncdWW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww011 Allowed
Histogram (7 states)
9334019:>2:r1=1; 2:r3=1; y=2;
84211603:>2:r1=1; 2:r3=1; y=1;
109651232:>2:r1=0; 2:r3=1; y=2;
133947176:>2:r1=0; 2:r3=0; y=1;
33680906:>2:r1=0; 2:r3=0; y=2;
14045933:>2:r1=0; 2:r3=1; y=1;
15129131:>2:r1=1; 2:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=d6dadb697329282571a4979eadd035fd
Cycle=SyncdRR Fre SyncdWW Wse SyncdWW Rfe
Relax bcsdww011 No BCSyncdWW
Safe=Fre Wse SyncdWW SyncdRR
Time bcsdww011 76.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww012
"SyncsRR Fre SyncdWW Wse SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r2) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1)
Generated assembler
_litmus_P2_0_: lwz 4,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww012 Allowed
Histogram (18 states)
28826 :>2:r1=0; 2:r3=1; x=2; y=1;
637401:>2:r1=2; 2:r3=1; x=1; y=1;
2404345:>2:r1=0; 2:r3=2; x=2; y=1;
578808:>2:r1=0; 2:r3=2; x=1; y=1;
2306223:>2:r1=1; 2:r3=2; x=1; y=2;
4225346:>2:r1=0; 2:r3=2; x=1; y=2;
753674:>2:r1=0; 2:r3=1; x=1; y=1;
4691075:>2:r1=2; 2:r3=1; x=2; y=1;
27709760:>2:r1=1; 2:r3=1; x=1; y=1;
11817096:>2:r1=0; 2:r3=1; x=1; y=2;
30090261:>2:r1=1; 2:r3=1; x=1; y=2;
57418164:>2:r1=0; 2:r3=0; x=1; y=1;
4728022:>2:r1=2; 2:r3=2; x=1; y=1;
95602588:>2:r1=2; 2:r3=2; x=2; y=1;
64945110:>2:r1=0; 2:r3=0; x=1; y=2;
34435193:>2:r1=0; 2:r3=0; x=2; y=1;
13086928:>2:r1=1; 2:r3=1; x=2; y=1;
44541180:>2:r1=2; 2:r3=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=3491c251ad1f32fc2b43d52f52c46191
Cycle=SyncsRR Fre SyncdWW Wse SyncdWW Rfe
Relax bcsdww012 No BCSyncdWW
Safe=Fre Wse SyncsRR SyncdWW
Time bcsdww012 76.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww013
"SyncdRW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | li r3,1 ;
li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | ;
exists (x=2 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww013 Allowed
Histogram (3 states)
125132891:>1:r1=0; x=1;
220347304:>1:r1=1; x=1;
294519805:>1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=3bacaa46622528b0ef100acb0d326a4f
Cycle=SyncdRW Wse SyncdWW Rfe
Relax bcsdww013 No BCSyncdWW
Safe=Wse SyncdRW
Time bcsdww013 77.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww014
"SyncdRW Wse SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | li r3,1 | sync | li r3,1 ;
li r3,1 | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: li 4,1
_litmus_P3_3_: stw 4,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww014 Allowed
Histogram (15 states)
266650:>1:r1=1; 3:r1=1; x=2; z=1;
361061:>1:r1=0; 3:r1=1; x=2; z=2;
349906:>1:r1=1; 3:r1=1; x=1; z=2;
11554328:>1:r1=1; 3:r1=0; x=1; z=2;
10429749:>1:r1=0; 3:r1=1; x=1; z=2;
9457772:>1:r1=0; 3:r1=0; x=1; z=1;
50748664:>1:r1=0; 3:r1=0; x=1; z=2;
38490309:>1:r1=0; 3:r1=1; x=1; z=1;
53106839:>1:r1=0; 3:r1=0; x=2; z=1;
21233930:>1:r1=1; 3:r1=1; x=1; z=1;
12395999:>1:r1=1; 3:r1=0; x=2; z=1;
41722059:>1:r1=1; 3:r1=0; x=1; z=1;
60077388:>1:r1=0; 3:r1=0; x=2; z=2;
9216210:>1:r1=0; 3:r1=1; x=2; z=1;
589136:>1:r1=1; 3:r1=0; x=2; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=ee6d6ba63625d467fac397c863618ff2
Cycle=SyncdRW Wse SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww014 No BCSyncdWW
Safe=Wse SyncdRW
Time bcsdww014 91.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww015
"DpdR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r3,1 | sync | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 10,30,30
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww015 Allowed
Histogram (15 states)
345880:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
656553:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
874654:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
1298905:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
18747242:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
31843823:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
50373704:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
40334530:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
5473744:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
14114251:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
12883118:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
24266876:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
9410324:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
66140745:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
43235651:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=17704085d61983610ea6761b47264366
Cycle=DpdR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww015 No BCSyncdWW
Safe=Fre Wse SyncdRW DpdR
Time bcsdww015 91.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww016
"DpsR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r3,1 | sync | lwzx r4,r3,r2 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: xor 10,4,4
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww016 Allowed
Histogram (42 states)
13 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
2175 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
14024 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
20065 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
38247 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
56766 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
14914 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
3665 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
14325 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
214793:>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
139882:>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
50040 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
22298 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
4398 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
63116 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
108640:>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
33150 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
520823:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
99654 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
4347884:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
1334723:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
38669 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
2939794:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
2304484:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
821250:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
2822903:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
284048:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
9484254:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
580157:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
3332788:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
15174712:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
10678503:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
36365718:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
54156421:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
27883011:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
27725022:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
36402789:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
18140040:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
10481712:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
8529788:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
17458361:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
27291981:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=afd72f686b99433de47ab6d5cad91134
Cycle=DpsR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww016 No BCSyncdWW
Safe=Fre Wse SyncdRW DpsR
Time bcsdww016 92.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww017
"SyncdRR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | li r3,1 | sync | lwz r3,0(r4) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww017 Allowed
Histogram (15 states)
344757:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
545657:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
39545350:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
46623603:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
64051817:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
494665:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
9476655:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
22102820:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
53118860:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
12617985:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
854127:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
14505814:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
12206475:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
35871778:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
7639637:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c13f8ec23ce3b9ee95f51b18bda82021
Cycle=SyncdRR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww017 No BCSyncdWW
Safe=Fre Wse SyncdRW SyncdRR
Time bcsdww017 94.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww018
"SyncsRR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | li r3,1 | sync | lwz r3,0(r2) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww018 Allowed
Histogram (42 states)
921 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
134574:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
451080:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
530601:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
192817:>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
299306:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
272423:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
408500:>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
579302:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
1926956:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
640368:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
3018494:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
1649820:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
482820:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
1801101:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
2889189:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
1456742:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
1114079:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
782112:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
1523518:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
185430:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
2697401:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
523202:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
906450:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
1962946:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
9293040:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
8348355:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
8571606:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
32083427:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
9110791:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
14454708:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
3319188:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
25318833:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
17639960:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
26109829:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
3376473:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
32890574:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
6028057:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
20917937:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
49992306:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
10434547:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
15680217:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=df82d53ff13c1c0132bc81937f5ecf56
Cycle=SyncsRR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww018 No BCSyncdWW
Safe=Fre Wse SyncsRR SyncdRW
Time bcsdww018 95.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww019
"DpdR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww019 Allowed
Histogram (3 states)
78974226:>1:r1=0; 1:r4=1;
320158660:>1:r1=0; 1:r4=0;
240867114:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r4=0) is NOT validated
Hash=abe769d43585052eb6bd1199546b3603
Cycle=DpdR Fre SyncdWW Rfe
Relax bcsdww019 No BCSyncdWW
Safe=Fre DpdR
Time bcsdww019 77.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww020
"DpdR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 | sync | lwzx r4,r3,r5 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 10,30,30
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww020 Allowed
Histogram (15 states)
1199870:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
1667482:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
1192991:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
17693891:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
16758472:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
1473874:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
40342175:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
17673784:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
29916043:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
71001590:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
16755120:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
31287469:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
31185904:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
40194444:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
1656891:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=ff6729203383abc4a32d53a80bd77acb
Cycle=DpdR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe
Relax bcsdww020 No BCSyncdWW
Safe=Fre DpdR
Time bcsdww020 90.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww021
"DpsR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 | sync | lwzx r4,r3,r2 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: xor 10,4,4
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww021 Allowed
Histogram (42 states)
13 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
5013 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
5613 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
24325 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
6494 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
84365 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
45866 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
39074 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
59666 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
134209:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
144301:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
82008 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
16889 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
214321:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
49379 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
24616 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
21430 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
27596 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
445131:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
973464:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
3704118:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
30704 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
553195:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
4420318:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
6327100:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
1084092:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
1783350:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
27477954:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
12898886:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
2980873:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
16018275:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
24208261:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
33351632:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
4703251:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
1662377:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
55469304:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
10458087:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
20365373:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
25340592:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
31977881:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
12662429:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
20118175:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=26085f29b1357e5e8f0e159288ddd725
Cycle=DpsR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe
Relax bcsdww021 No BCSyncdWW
Safe=Fre DpsR DpdR
Time bcsdww021 93.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww022
"SyncdRR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r5 | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww022 Allowed
Histogram (15 states)
1031325:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
1070595:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
773071:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
14490300:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
31658618:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
23446630:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
437204:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
4217867:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
12493434:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
46992199:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
16028464:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
45486767:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
36099357:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
71940925:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
13833244:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=52b75bc6c8456215cdaad6fb3a5164ee
Cycle=SyncdRR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe
Relax bcsdww022 No BCSyncdWW
Safe=Fre SyncdRR DpdR
Time bcsdww022 90.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww023
"SyncsRR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r5 | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww023 Allowed
Histogram (42 states)
1904 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
508083:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
227799:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
327855:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1367295:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
1445777:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
746302:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
363210:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
706225:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
1850606:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
1349033:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
435080:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
1189033:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
5103703:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
946831:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
927902:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
3497643:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
4750921:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
295113:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
3485890:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
1461379:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
196345:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
5988088:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
2782038:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
19796947:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
25954810:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
21861809:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
919586:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
17596939:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
19384851:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
453736:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
51599553:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
11904148:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
2500193:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
11985157:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
15748183:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
1855790:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
28998465:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
10078552:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
29278710:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
2430050:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
7698466:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=ef69b708c957de42a04a8b5ca4d81078
Cycle=SyncsRR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe
Relax bcsdww023 No BCSyncdWW
Safe=Fre SyncsRR DpdR
Time bcsdww023 95.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww024
"DpsR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r2 | sync | lwzx r4,r3,r2 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: xor 10,4,4
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww024 Allowed
Histogram (103 states)
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
33 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
10 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
90 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
25 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
56 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
39 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
75 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
17 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
127 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
26 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
70 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
51 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
91 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
73 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
57 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
16 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
240 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
179 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=1;
218 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
68 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
710 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
17 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
5965 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
96 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
4327 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
779 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
57950 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
71364 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
6145 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
4163 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
13653 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
13042 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
68403 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
51138 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
17634 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
13878 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
7785 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
4153 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
4501 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
56749 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
34882 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
7157 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
13766 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
7077 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
13460 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
47444 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
53306 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
42920 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
49824 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
14817 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
36144 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
72573 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
50007 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
8111 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
13074 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
35691 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
61069 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
47496 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
68797 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
272315:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
37256 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
90151 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
148406:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
25785 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
125960:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
38223 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
1753351:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
3135814:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
3893378:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
9394671:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
2621116:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
6449145:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
478638:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
118381:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
6457061:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
7793416:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
2771319:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
474124:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
1738074:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
4524728:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
210407:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
382721:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
3248546:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
130578:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
21933242:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
27275071:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
3945036:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
4623906:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
21623720:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
7746038:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
23996984:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
7696013:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
775028:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
22528791:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
27173911:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
9425639:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
24327821:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
37024414:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
22509188:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=6e01edb2061b004b7156eefd80367964
Cycle=DpsR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe
Relax bcsdww024 No BCSyncdWW
Safe=Fre DpsR
Time bcsdww024 105.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww025
"SyncdRR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r2 | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww025 Allowed
Histogram (42 states)
60 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
8619 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
7619 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
16731 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
46814 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
25032 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
22278 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
55826 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
89650 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
48444 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
339943:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
220264:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
30124 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
81482 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
156560:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
79247 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
624175:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
103742:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
166138:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
1489060:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
3874738:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
1269414:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
46625 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
3135458:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
6927326:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
626039:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
602888:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
2635919:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
2218485:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
4852786:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
12689941:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
26413938:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
18446820:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
25657992:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
36664512:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
12312019:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
19597430:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
33852774:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
12487256:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
25505547:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
55145020:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
11425265:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=f58b58e77c065c1d7e45eddd6a49ef4b
Cycle=SyncdRR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe
Relax bcsdww025 No BCSyncdWW
Safe=Fre SyncdRR DpsR
Time bcsdww025 93.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww026
"SyncsRR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r2 | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww026 Allowed
Histogram (108 states)
6 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
7 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
8 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
5 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
19 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
447 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
287 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
127 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
478 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1994 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
989 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
5161 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
4655 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
1399 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
268 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
849 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
37 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
755 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
4947 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
913 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
143 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
2451 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
3464 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
6889 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
2098 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
8658 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
13898 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
704 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
3680 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
1077 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
4789 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
61602 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
19367 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
120 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
35105 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
6860 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
13965 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
54756 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
38591 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
4002 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
42869 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
17003 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
81244 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
13467 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
33911 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
67548 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
20908 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
7404 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
49003 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
10489 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
104308:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
238240:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
823341:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
425520:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
82195 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
743836:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
131340:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
237144:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
474921:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
298495:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
836693:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
859004:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
2101968:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
831964:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
569563:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
135689:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
769799:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
3047472:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
32154 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
1613308:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
3451242:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
147302:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
2276011:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
869153:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
1405259:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
640211:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
3940827:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
423270:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
2436399:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
7194592:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
1290319:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
5294312:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
5027219:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
562572:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
1499996:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
688198:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
2305343:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
459334:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
3793726:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
1188209:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
6303771:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
20305245:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
21662744:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
35004702:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
3325009:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
20790048:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
6256120:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
8959537:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
2941058:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
18751749:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
7601363:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
2237916:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
3996855:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
23608012:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
8800264:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
24754388:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
24753203:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
20048152:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=494bdd377023c801c91266ccd04985a6
Cycle=SyncsRR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe
Relax bcsdww026 No BCSyncdWW
Safe=Fre SyncsRR DpsR
Time bcsdww026 105.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww027
"DpdW Wse SyncdWR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | li r4,1 ;
lwz r3,0(r4) | li r3,1 | stwx r4,r3,r5 ;
| stw r3,0(r4) | ;
exists (x=2 /\ 0:r3=0 /\ 2:r1=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 31,2
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww027 Allowed
Histogram (7 states)
5324432:>0:r3=1; 2:r1=0; x=1;
21956978:>0:r3=1; 2:r1=1; x=2;
55840858:>0:r3=0; 2:r1=0; x=2;
108874039:>0:r3=0; 2:r1=0; x=1;
102450506:>0:r3=1; 2:r1=0; x=2;
22670157:>0:r3=0; 2:r1=1; x=1;
82883030:>0:r3=1; 2:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=1) is NOT validated
Hash=a3cc59f896bd23424085486bc047f237
Cycle=DpdW Wse SyncdWR Fre SyncdWW Rfe
Relax bcsdww027 No BCSyncdWW
Safe=Fre Wse SyncdWR DpdW
Time bcsdww027 71.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww028
"SyncdRW Wse SyncdWR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | li r3,1 ;
lwz r3,0(r4) | li r3,1 | stw r3,0(r4) ;
| stw r3,0(r4) | ;
exists (x=2 /\ 0:r3=0 /\ 2:r1=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 31,2
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww028 Allowed
Histogram (7 states)
12147222:>0:r3=1; 2:r1=1; x=2;
12007944:>0:r3=1; 2:r1=0; x=1;
113884517:>0:r3=1; 2:r1=0; x=2;
127759113:>0:r3=0; 2:r1=0; x=1;
40361849:>0:r3=0; 2:r1=0; x=2;
78265461:>0:r3=1; 2:r1=1; x=1;
15573894:>0:r3=0; 2:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=1) is NOT validated
Hash=e4e07528cdbf9272fd50b0cf6708ccaa
Cycle=SyncdRW Wse SyncdWR Fre SyncdWW Rfe
Relax bcsdww028 No BCSyncdWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcsdww028 77.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww029
"DpdR Fre SyncdWR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r5 ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (0:r3=0 /\ 2:r1=1 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww029 Allowed
Histogram (7 states)
4401668:>0:r3=1; 2:r1=0; 2:r4=1;
23415476:>0:r3=1; 2:r1=1; 2:r4=0;
111347821:>0:r3=0; 2:r1=0; 2:r4=1;
109545702:>0:r3=1; 2:r1=0; 2:r4=0;
53627666:>0:r3=0; 2:r1=0; 2:r4=0;
19861287:>0:r3=0; 2:r1=1; 2:r4=1;
77800380:>0:r3=1; 2:r1=1; 2:r4=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=1052dfbfb336d023eeffaaf6c00324c1
Cycle=DpdR Fre SyncdWR Fre SyncdWW Rfe
Relax bcsdww029 No BCSyncdWW
Safe=Fre SyncdWR DpdR
Time bcsdww029 77.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww030
"DpsR Fre SyncdWR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r2 ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r4=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 11,10,9
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww030 Allowed
Histogram (18 states)
1477 :>0:r3=0; 2:r1=0; 2:r4=1; y=1;
2147 :>0:r3=1; 2:r1=2; 2:r4=1; y=1;
403784:>0:r3=0; 2:r1=2; 2:r4=1; y=1;
53266 :>0:r3=1; 2:r1=0; 2:r4=2; y=1;
13404 :>0:r3=1; 2:r1=1; 2:r4=2; y=2;
75281 :>0:r3=1; 2:r1=0; 2:r4=1; y=1;
304137:>0:r3=1; 2:r1=0; 2:r4=2; y=2;
100864:>0:r3=0; 2:r1=0; 2:r4=2; y=1;
711024:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
15148767:>0:r3=1; 2:r1=1; 2:r4=1; y=1;
37836118:>0:r3=1; 2:r1=0; 2:r4=0; y=1;
46160308:>0:r3=1; 2:r1=2; 2:r4=2; y=2;
2569177:>0:r3=1; 2:r1=2; 2:r4=2; y=1;
42557483:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
106283653:>0:r3=0; 2:r1=2; 2:r4=2; y=1;
55436938:>0:r3=0; 2:r1=0; 2:r4=0; y=1;
23591910:>0:r3=0; 2:r1=1; 2:r4=1; y=1;
68750262:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=762db7307d35c050ae02494154891df7
Cycle=DpsR Fre SyncdWR Fre SyncdWW Rfe
Relax bcsdww030 No BCSyncdWW
Safe=Fre SyncdWR DpsR
Time bcsdww030 79.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww031
"SyncdRR Fre SyncdWR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww031 Allowed
Histogram (7 states)
7790240:>0:r3=1; 2:r1=0; 2:r3=1;
75772489:>0:r3=1; 2:r1=1; 2:r3=1;
115746000:>0:r3=0; 2:r1=0; 2:r3=1;
115386726:>0:r3=1; 2:r1=0; 2:r3=0;
17109796:>0:r3=0; 2:r1=1; 2:r3=1;
16746993:>0:r3=1; 2:r1=1; 2:r3=0;
51447756:>0:r3=0; 2:r1=0; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=d99b2c9fcd24d521255a6c4ef185df57
Cycle=SyncdRR Fre SyncdWR Fre SyncdWW Rfe
Relax bcsdww031 No BCSyncdWW
Safe=Fre SyncdWR SyncdRR
Time bcsdww031 75.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww032.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww032
"SyncsRR Fre SyncdWR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r2) ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=1)
Generated assembler
_litmus_P2_0_: lwz 4,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww032 Allowed
Histogram (18 states)
319495:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
48843 :>0:r3=0; 2:r1=0; 2:r3=1; y=1;
1882562:>0:r3=0; 2:r1=0; 2:r3=2; y=1;
2047441:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
53996930:>0:r3=0; 2:r1=0; 2:r3=0; y=1;
293070:>0:r3=1; 2:r1=2; 2:r3=1; y=1;
10499126:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
3542075:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
4981033:>0:r3=0; 2:r1=2; 2:r3=1; y=1;
29926410:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
68599222:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
43066877:>0:r3=1; 2:r1=2; 2:r3=2; y=2;
581441:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
21988751:>0:r3=0; 2:r1=1; 2:r3=1; y=1;
2898612:>0:r3=1; 2:r1=2; 2:r3=2; y=1;
103448865:>0:r3=0; 2:r1=2; 2:r3=2; y=1;
37649421:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
14229826:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=6ef8013c1a65c6c1574ee921baad8f97
Cycle=SyncsRR Fre SyncdWR Fre SyncdWW Rfe
Relax bcsdww032 No BCSyncdWW
Safe=Fre SyncsRR SyncdWR
Time bcsdww032 79.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww033.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww033
"SyncdRR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww033 Allowed
Histogram (3 states)
107076267:>1:r1=0; 1:r3=1;
308314832:>1:r1=0; 1:r3=0;
224608901:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=6fa2fc8a03a8948f9262ae5fd1e47a19
Cycle=SyncdRR Fre SyncdWW Rfe
Relax bcsdww033 No BCSyncdWW
Safe=Fre SyncdRR
Time bcsdww033 75.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww034.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww034
"SyncdRR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww034 Allowed
Histogram (15 states)
613584:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
11322711:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
429495:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
497950:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
6293100:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
13401984:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
70945478:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
34696361:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
35591005:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
12408101:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
50338192:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
13099839:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
48689954:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
20869700:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
802546:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=3dd9d4fff43138f32cd2819c7a65cdb3
Cycle=SyncdRR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe
Relax bcsdww034 No BCSyncdWW
Safe=Fre SyncdRR
Time bcsdww034 93.80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww035.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww035
"SyncsRR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww035 Allowed
Histogram (42 states)
1210 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
362911:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
369275:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
295996:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
522656:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
529615:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
225137:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1832532:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1186007:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
183451:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
417743:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
499004:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
2269611:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
2753724:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
3238278:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
1834178:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
248990:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
7070943:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
2122768:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
986195:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2128320:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
888942:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
3179660:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
12239493:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
7489602:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1414420:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
3667388:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
1322660:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
504824:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
52045383:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
29874698:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
24849180:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
9657863:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
19663919:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
12575235:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
15730278:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
5666640:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
24122831:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
691747:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
11533933:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
33756722:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
20046038:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=f0c1b6d32c1c64645b39ad490ac97524
Cycle=SyncsRR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe
Relax bcsdww035 No BCSyncdWW
Safe=Fre SyncsRR SyncdRR
Time bcsdww035 94.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww036.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww036
"DpdR Fre SyncsWR Fre SyncdWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (x=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test bcsdww036 Allowed
Histogram (13 states)
159339:>0:r3=2; 2:r1=0; 2:r4=1; x=2;
1677100:>0:r3=2; 2:r1=1; 2:r4=2; x=2;
1116023:>0:r3=2; 2:r1=0; 2:r4=2; x=2;
7588326:>0:r3=1; 2:r1=0; 2:r4=1; x=1;
65843434:>0:r3=1; 2:r1=0; 2:r4=0; x=1;
6135187:>0:r3=2; 2:r1=0; 2:r4=0; x=2;
46751825:>0:r3=1; 2:r1=0; 2:r4=2; x=1;
65077327:>0:r3=1; 2:r1=0; 2:r4=1; x=2;
52938827:>0:r3=1; 2:r1=0; 2:r4=2; x=2;
11089456:>0:r3=1; 2:r1=1; 2:r4=2; x=1;
60016705:>0:r3=1; 2:r1=0; 2:r4=0; x=2;
13431371:>0:r3=1; 2:r1=1; 2:r4=2; x=2;
68175080:>0:r3=1; 2:r1=1; 2:r4=1; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=b5668ea36c70858ef8634a895265c398
Cycle=DpdR Fre SyncsWR Fre SyncdWW Rfe
Relax bcsdww036 No BCSyncdWW
Safe=Fre SyncsWR DpdR
Time bcsdww036 75.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww037.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww037
"SyncdRR Fre SyncsWR Fre SyncdWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (x=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test bcsdww037 Allowed
Histogram (13 states)
119358:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
2013734:>0:r3=2; 2:r1=1; 2:r3=2; x=2;
1070443:>0:r3=2; 2:r1=0; 2:r3=2; x=2;
42077967:>0:r3=1; 2:r1=0; 2:r3=2; x=1;
7973194:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
8672934:>0:r3=1; 2:r1=0; 2:r3=1; x=1;
54469716:>0:r3=1; 2:r1=0; 2:r3=2; x=2;
14863855:>0:r3=1; 2:r1=1; 2:r3=2; x=1;
62788985:>0:r3=1; 2:r1=0; 2:r3=0; x=1;
64241711:>0:r3=1; 2:r1=0; 2:r3=1; x=2;
57026761:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
70256537:>0:r3=1; 2:r1=1; 2:r3=1; x=1;
14424805:>0:r3=1; 2:r1=1; 2:r3=2; x=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=c99d291fc8d3f66519c556e43131cb0b
Cycle=SyncdRR Fre SyncsWR Fre SyncdWW Rfe
Relax bcsdww037 No BCSyncdWW
Safe=Fre SyncsWR SyncdRR
Time bcsdww037 75.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww038.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww038
"SyncsRR Fre SyncdWW Rfe SyncsRR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r2) | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 11,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww038 Allowed
Histogram (108 states)
1114 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
393 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
1945 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1713 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
411 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
2407 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
15604 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
13708 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
95117 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
1949 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
9214 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
4119 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
67329 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
32067 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
134432:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
1286 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
33536 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
13981 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
20295 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
129012:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
90438 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
24365 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
18838 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
33563 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
63017 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
197813:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
747697:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
34639 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
8023 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
214860:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
133498:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
53202 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
6951 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
25534 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
126300:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
739830:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
396156:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
236939:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
559209:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
666950:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
582336:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
82214 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
517569:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
626266:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
423073:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1345314:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
83325 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
575297:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
125018:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
3421019:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
306431:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
1160354:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
515494:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
497857:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
741350:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
466148:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
728035:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
1173298:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
8723426:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
6223278:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1105537:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
1328044:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
2075443:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
1020384:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
302818:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
4052508:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
639890:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
2892579:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
400183:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
172539:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
3577793:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
2224965:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
174211:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
601603:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
3322448:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
5926213:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1782197:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2050207:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
1098815:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
807589:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
562349:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
6314673:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
2095468:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
6461405:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
2128810:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2129879:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
2039670:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1386612:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
728999:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
400588:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1091502:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
846459:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
140117:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
2889419:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
6271455:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
3664294:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
19046665:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
20552484:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
18667544:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
22684923:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
23253436:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
32818055:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
8749978:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2244330:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
20069911:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
19663569:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
3954973:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
20311911:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=1749371cc26417072606d04b91651c05
Cycle=SyncsRR Fre SyncdWW Rfe SyncsRR Fre SyncdWW Rfe
Relax bcsdww038 No BCSyncdWW
Safe=Fre SyncsRR
Time bcsdww038 108.66
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Wed Dec 23 17:23:44 GMT 2009