Thu Dec 31 14:52:37 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 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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 bcsdww000 Allowed
Histogram (3 states)
493697170:>1:r1=1; x=1;
626123296:>1:r1=0; x=2;
160179534:>1:r1=0; x=1;
No
Witnesses
Positive: 0, Negative: 1280000000
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 90.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,3,3
_litmus_P3_2_: li 10,1
_litmus_P3_3_: stwx 10,30,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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)
1470933:>1:r1=1; 3:r1=1; x=1; z=2;
2364108:>1:r1=1; 3:r1=0; x=2; z=2;
1552483:>1:r1=1; 3:r1=1; x=2; z=1;
5191426:>1:r1=0; 3:r1=0; x=1; z=1;
86021271:>1:r1=0; 3:r1=0; x=1; z=2;
58503357:>1:r1=1; 3:r1=1; x=1; z=1;
27672307:>1:r1=1; 3:r1=0; x=2; z=1;
3266744:>1:r1=0; 3:r1=1; x=2; z=2;
34995927:>1:r1=0; 3:r1=1; x=2; z=1;
61525394:>1:r1=1; 3:r1=0; x=1; z=1;
83436597:>1:r1=0; 3:r1=0; x=2; z=1;
34583195:>1:r1=0; 3:r1=1; x=1; z=2;
68324466:>1:r1=0; 3:r1=1; x=1; z=1;
30440231:>1:r1=1; 3:r1=0; x=1; z=2;
140651561:>1:r1=0; 3:r1=0; x=2; z=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 177.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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)
1462568:>1:r1=1; 3:r1=1; x=1; z=2;
745713:>1:r1=1; 3:r1=1; x=2; z=1;
2044255:>1:r1=1; 3:r1=0; x=2; z=2;
26968124:>1:r1=1; 3:r1=0; x=2; z=1;
1649905:>1:r1=0; 3:r1=1; x=2; z=2;
31800443:>1:r1=1; 3:r1=0; x=1; z=2;
29187606:>1:r1=0; 3:r1=1; x=1; z=2;
67809777:>1:r1=0; 3:r1=1; x=1; z=1;
22333660:>1:r1=0; 3:r1=1; x=2; z=1;
10389149:>1:r1=0; 3:r1=0; x=1; z=1;
51762105:>1:r1=1; 3:r1=1; x=1; z=1;
99512810:>1:r1=0; 3:r1=0; x=1; z=2;
87827466:>1:r1=0; 3:r1=0; x=2; z=1;
77703917:>1:r1=1; 3:r1=0; x=1; z=1;
128802502:>1:r1=0; 3:r1=0; x=2; z=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 174.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P3_1_: xor 10,28,28
_litmus_P3_2_: lwzx 30,10,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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)
849664:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
1592933:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
1387246:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
3618500:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
35873170:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
35000441:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
50029984:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
5930747:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
94305297:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
85464447:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
72327141:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
20828197:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
148200205:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
59662667:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
24929361:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 168.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(9)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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 bcsdww004 Allowed
Histogram (42 states)
37 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
11389 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
6499 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
9871 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
66280 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
372716:>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
26197 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
242510:>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
93161 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
81800 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
66361 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
161798:>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
10149 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
89631 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
184708:>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
48170 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
96526 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
37792 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
1072786:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
264497:>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
1075072:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
3706796:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
1897157:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
20708625:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
13392693:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
66832816:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
42731237:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
6200655:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
9510694:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
22783251:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
55378521:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
3379090:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
7445440:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
31836864:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
38826395:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
51794755:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
27411250:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
63198422:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
48305978:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
8663781:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
2476082:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
109501548:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 180.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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)
1414528:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1964731:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
7162048:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
2296261:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
29680734:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
32969345:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
28471992:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
84812991:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
56329301:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
33859435:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
2632206:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
134572177:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
62401773:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
72465429:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
88967049:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 170.70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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 bcsdww006 Allowed
Histogram (42 states)
3418 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
641146:>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
379124:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
766809:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
438896:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
495092:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
2065779:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
649234:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
7138479:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
453045:>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
2802660:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
2593605:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
709980:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
8724483:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
1681726:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
1348403:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1329108:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
2977559:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
1866876:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
2696647:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
2881704:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
5957271:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
14127766:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
3265002:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
7014710:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
39627329:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
4460334:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
4867421:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
10959431:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
54543673:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
11293657:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
52189901:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
61669814:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
40971188:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
1943795:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
101274496:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
33199090:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
18521479:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
22696872:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
37818078:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
26411939:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
44542981:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 183.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: xor 30,28,28
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,30,9
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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)
42498328:>2:r1=1; x=2; y=1;
21698627:>2:r1=0; x=1; y=1;
211281767:>2:r1=0; x=1; y=2;
68980110:>2:r1=0; x=2; y=2;
180628584:>2:r1=1; x=1; y=1;
247142765:>2:r1=0; x=2; y=1;
27769819:>2:r1=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 115.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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)
27188968:>2:r1=1; x=2; y=1;
21628792:>2:r1=1; x=1; y=2;
32241797:>2:r1=0; x=1; y=1;
52307100:>2:r1=0; x=2; y=2;
176664189:>2:r1=1; x=1; y=1;
255409202:>2:r1=0; x=2; y=1;
234559952:>2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 118.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: xor 10,28,28
_litmus_P2_2_: lwzx 30,10,9
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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)
17146576:>2:r1=1; 2:r4=1; y=2;
24653169:>2:r1=0; 2:r4=1; y=1;
159462997:>2:r1=1; 2:r4=1; y=1;
284381498:>2:r1=0; 2:r4=0; y=1;
27261687:>2:r1=1; 2:r4=0; y=1;
73026263:>2:r1=0; 2:r4=0; y=2;
214067810:>2:r1=0; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 115.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 11,10,9
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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 bcsdww010 Allowed
Histogram (18 states)
1259 :>2:r1=0; 2:r4=1; x=2; y=1;
43510 :>2:r1=1; 2:r4=2; x=1; y=2;
16679 :>2:r1=2; 2:r4=1; x=1; y=1;
70014 :>2:r1=0; 2:r4=2; x=2; y=1;
251014:>2:r1=0; 2:r4=2; x=1; y=1;
493163:>2:r1=2; 2:r4=1; x=2; y=1;
319636:>2:r1=0; 2:r4=1; x=1; y=1;
1321752:>2:r1=0; 2:r4=2; x=1; y=2;
32956217:>2:r1=1; 2:r4=1; x=2; y=1;
59518466:>2:r1=1; 2:r4=1; x=1; y=1;
1993133:>2:r1=0; 2:r4=1; x=1; y=2;
11364715:>2:r1=2; 2:r4=2; x=1; y=1;
114232127:>2:r1=0; 2:r4=0; x=1; y=1;
76230288:>2:r1=1; 2:r4=1; x=1; y=2;
143534299:>2:r1=0; 2:r4=0; x=1; y=2;
75493180:>2:r1=0; 2:r4=0; x=2; y=1;
191496681:>2:r1=2; 2:r4=2; x=2; y=1;
90663867:>2:r1=2; 2:r4=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 116.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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)
16738274:>2:r1=1; 2:r3=1; y=2;
67808275:>2:r1=0; 2:r3=0; y=2;
22654317:>2:r1=1; 2:r3=0; y=1;
28695150:>2:r1=0; 2:r3=1; y=1;
161965915:>2:r1=1; 2:r3=1; y=1;
220098356:>2:r1=0; 2:r3=1; y=2;
282039713:>2:r1=0; 2:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 115.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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 bcsdww012 Allowed
Histogram (18 states)
55670 :>2:r1=0; 2:r3=1; x=2; y=1;
9284377:>2:r1=2; 2:r3=1; x=2; y=1;
3875686:>2:r1=0; 2:r3=2; x=2; y=1;
29159216:>2:r1=1; 2:r3=1; x=2; y=1;
59073010:>2:r1=1; 2:r3=1; x=1; y=1;
1037645:>2:r1=0; 2:r3=2; x=1; y=1;
23313588:>2:r1=0; 2:r3=1; x=1; y=2;
1139213:>2:r1=2; 2:r3=1; x=1; y=1;
1375797:>2:r1=0; 2:r3=1; x=1; y=1;
9602995:>2:r1=2; 2:r3=2; x=1; y=1;
4698390:>2:r1=1; 2:r3=2; x=1; y=2;
8432440:>2:r1=0; 2:r3=2; x=1; y=2;
73026117:>2:r1=0; 2:r3=0; x=2; y=1;
106985104:>2:r1=0; 2:r3=0; x=1; y=1;
86233257:>2:r1=2; 2:r3=2; x=1; y=2;
186957609:>2:r1=2; 2:r3=2; x=2; y=1;
137153059:>2:r1=0; 2:r3=0; x=1; y=2;
58596827:>2:r1=1; 2:r3=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 121.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: 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 bcsdww013 Allowed
Histogram (3 states)
295034918:>1:r1=0; x=1;
399801763:>1:r1=1; x=1;
585163319:>1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 1280000000
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 92.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,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 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)
1173532:>1:r1=1; 3:r1=0; x=2; z=2;
777864:>1:r1=1; 3:r1=1; x=2; z=1;
1090973:>1:r1=0; 3:r1=1; x=2; z=2;
845614:>1:r1=1; 3:r1=1; x=1; z=2;
15529610:>1:r1=0; 3:r1=0; x=1; z=1;
46808908:>1:r1=1; 3:r1=1; x=1; z=1;
24976335:>1:r1=1; 3:r1=0; x=2; z=1;
23234762:>1:r1=0; 3:r1=1; x=2; z=1;
99107472:>1:r1=0; 3:r1=0; x=1; z=2;
78501149:>1:r1=1; 3:r1=0; x=1; z=1;
23507792:>1:r1=1; 3:r1=0; x=1; z=2;
121324677:>1:r1=0; 3:r1=0; x=2; z=2;
78184207:>1:r1=0; 3:r1=1; x=1; z=1;
23796955:>1:r1=0; 3:r1=1; x=1; z=2;
101140150:>1:r1=0; 3:r1=0; x=2; z=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 176.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P3_1_: xor 10,28,28
_litmus_P3_2_: lwzx 30,10,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,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 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)
1333702:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
1652812:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
678264:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
9724708:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
26382195:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
18966114:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
50353300:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
88392069:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
28879600:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
2510076:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
81253955:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
131027865:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
63135235:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
98319852:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
37390253:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 167.78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(9)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,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 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 bcsdww016 Allowed
Histogram (42 states)
43 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
5385 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
9435 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
6593 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
360582:>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
73469 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
27916 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
27543 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
53375 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
195781:>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
40140 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
288055:>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
33876 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
200220:>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
999615:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
107017:>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
97815 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
143994:>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
82672 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
40733 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
5514965:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
5615044:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
22960730:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
737278:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
5170828:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
6740308:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
1063062:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
1931259:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
3217110:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
20138734:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
29071310:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
10144384:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
22194485:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
53765986:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
71161095:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
70628664:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
17285446:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
107150462:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
56080305:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
34565758:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
37821003:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
54247525:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 178.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,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 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)
813049:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
14021729:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
1169469:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
1619099:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
1192828:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
25082013:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
28492483:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
92588502:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
104478931:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
76411891:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
21088670:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
128283905:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
45911764:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
72731767:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
26113900:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 166.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,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 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 bcsdww018 Allowed
Histogram (42 states)
2003 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
385871:>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
706508:>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
1026201:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
623372:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
410434:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
1016557:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
3735999:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
334966:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
2578320:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
5525506:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
1326387:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
5252771:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
3227590:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
1095380:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
3652298:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
731311:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
1161924:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1498749:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
2884891:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
2309346:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
6751803:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
21074772:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
27298843:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
2156904:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
4516418:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
4951607:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
15577267:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
11144716:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
20608075:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
32876267:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
41977204:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
34287779:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
53616294:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
49508176:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
62770644:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
725742:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
65430574:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
100758658:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
20461406:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
15972628:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
8047839:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 182.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
234937663:>1:r1=0; 1:r4=1;
639724570:>1:r1=0; 1:r4=0;
405337767:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 1280000000
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 90.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3393229:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
3488487:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
3024944:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
2274763:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
32795798:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
32455392:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
2128593:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
35249346:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
34917200:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
63110441:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
81147801:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
61406734:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
140717781:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
83811897:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
60077594:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 171.80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(9)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,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 bcsdww021 Allowed
Histogram (42 states)
96 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
5906 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
4925 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
9258 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
17689 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
9198 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
259499:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
59035 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
234708:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
110676:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
90132 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
46573 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
58600 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
171982:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
81378 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
139141:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
286841:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
133240:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
67509 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
1149594:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
1713020:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
3873258:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
1342109:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
6519105:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
3533299:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
25576374:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
35328000:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
41306987:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
47896273:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
27636676:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
8108275:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
13608108:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
7046236:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
2353212:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
66715856:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
41591119:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
8627319:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
18655446:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
109297476:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
64829675:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
53117274:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
48388923:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 182.87
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1434302:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
2086095:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
2264527:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
3020405:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
7065625:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
29109615:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
26466093:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
86958281:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
88226515:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
60636930:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
35694055:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
138031027:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
53561909:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
72086391:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
33358230:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 640000000
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 165.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,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 bcsdww023 Allowed
Histogram (42 states)
3563 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
498409:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
694543:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
363342:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
2795455:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
1694067:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
2939317:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
6450138:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
2990068:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
2800947:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1495293:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
4251700:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
8910582:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
651023:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
22972187:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
531896:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
880970:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
1896266:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
1134795:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
3730251:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
1839295:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
3163285:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
838935:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
35070168:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
10429537:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
5327406:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
7263127:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
5570009:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1702986:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
36615244:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
39239532:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
16682003:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
43053180:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
12172774:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
19400988:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
33180671:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
2195389:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
25336662:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
57150821:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
103870206:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
52004646:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
60208324:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 179.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(9)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,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,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 bcsdww024 Allowed
Histogram (106 states)
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
5 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
10 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
5 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
5 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
41 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
35 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
59 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
136 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
152 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
108 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
204 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
156 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
15 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
233 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
179 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
129 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
52 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
192 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
257 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
174 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
191 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
94 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
112 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
1848 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
613 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=1;
12206 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
10329 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
8437 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
1818 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
119240:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
142329:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
99668 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
8812 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
29370 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
18707 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
142 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
125198:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
148946:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
97192 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
19450 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
29827 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
10441 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
11717 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
31088 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
73290 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
18658 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
127654:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
592 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
19431 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
202126:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
30045 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
75112 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
148545:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
27477 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
200978:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
666936:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
26415 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
1343385:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
67187 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
903487:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
141579:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
66476 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
338704:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
149697:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
3726339:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
5326644:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
144026:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
18880 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
13636001:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
99191 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
129476:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
18871 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
47762 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
254272:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
673836:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
6023113:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
5249105:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
255580:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
15920197:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
5990498:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
3747384:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
8352353:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
338903:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
908330:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
53694311:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
49443896:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
73418759:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
98755 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
18888384:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
8314633:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
44687594:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
42538581:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
48085 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
18835035:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
53897151:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
44906154:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
15035768:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
9452021:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
42740954:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
49432479:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
15083804:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
13620310:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
9444865:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 218.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,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)
51 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
7645 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
8186 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
28612 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
148866:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
50170 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
28385 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
43697 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
415545:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
12227 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
100566:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
78198 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
196030:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
45041 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
42678 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
101027:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
296229:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
85985 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
1013523:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
5386321:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
1381866:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
3366366:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
2705261:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
991842:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
236714:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
13866448:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
108959871:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
6548989:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
38497352:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
52372675:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
24469271:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
8019770:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
52102353:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
38713485:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
4226664:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
25597622:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
66132598:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
51397594:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
72566447:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
23520020:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
10632118:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
25605692:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 173.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,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,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 bcsdww026 Allowed
Histogram (108 states)
5 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
16 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
21 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
104 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
11 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
282 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
16004 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
80 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
6426 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
898 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
1278 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
1829 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
948 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
745 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
162 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
1159 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
566 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
11459 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
349 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
3806 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
2288 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
38972 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
1834 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
145103:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
11174 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
17763 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
7033 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
28220 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
7737 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
143470:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
5601 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
26030 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
9745 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
2437 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
81770 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
32808 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
8148 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
22442 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
228441:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
19593 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
1747112:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
263962:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
28626 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
86935 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
16572 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
34504 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
176203:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
117683:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
11038 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
1634760:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
644306:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
65291 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
1355724:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
6789 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
1456800:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
1191930:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
181451:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
603107:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
406598:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
4417394:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
273965:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
1558656:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
1008792:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
1508702:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
700880:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
62429 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
43620 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
385733:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
5927640:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
1686965:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
1175922:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
870589:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
72769 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
114949:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
6638252:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
2385743:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
11034802:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
14290094:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
3439514:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
2544708:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
2918938:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
3273961:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
4420495:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
10054626:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
15187798:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
5790041:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
12725252:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
42279533:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
43014880:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
2966961:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
6723265:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
48809817:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
37897222:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
17792563:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
1598289:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
69839200:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
49993184:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
4392730:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
18449997:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
7518290:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
13427173:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
7974170:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
47738020:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
7441736:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
41139794:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
39813360:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
1347249:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
4413190:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 235.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: xor 30,28,28
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,30,9
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww027 Allowed
Histogram (7 states)
13016293:>0:r3=1; 2:r1=0; x=1;
41033872:>0:r3=0; 2:r1=1; x=1;
109500839:>0:r3=0; 2:r1=0; x=2;
42950830:>0:r3=1; 2:r1=1; x=2;
223822535:>0:r3=0; 2:r1=0; x=1;
208980995:>0:r3=1; 2:r1=0; x=2;
160694636:>0:r3=1; 2:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 115.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww028 Allowed
Histogram (7 states)
31524167:>0:r3=0; 2:r1=1; x=1;
25745694:>0:r3=1; 2:r1=0; x=1;
81347190:>0:r3=0; 2:r1=0; x=2;
157831834:>0:r3=1; 2:r1=1; x=1;
253548798:>0:r3=0; 2:r1=0; x=1;
223839729:>0:r3=1; 2:r1=0; x=2;
26162588:>0:r3=1; 2:r1=1; x=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 112.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
9232925:>0:r3=1; 2:r1=0; 2:r4=1;
47250231:>0:r3=0; 2:r1=1; 2:r4=1;
157294376:>0:r3=1; 2:r1=1; 2:r4=1;
109352074:>0:r3=0; 2:r1=0; 2:r4=0;
212546151:>0:r3=1; 2:r1=0; 2:r4=0;
214911553:>0:r3=0; 2:r1=0; 2:r4=1;
49412690:>0:r3=1; 2:r1=1; 2:r4=0;
No
Witnesses
Positive: 0, Negative: 800000000
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 121.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 11,10,9
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww030 Allowed
Histogram (18 states)
1854 :>0:r3=1; 2:r1=2; 2:r4=1; y=1;
3454 :>0:r3=0; 2:r1=0; 2:r4=1; y=1;
43449 :>0:r3=0; 2:r1=0; 2:r4=2; y=1;
6748 :>0:r3=1; 2:r1=1; 2:r4=2; y=2;
185103:>0:r3=1; 2:r1=0; 2:r4=2; y=1;
329869:>0:r3=0; 2:r1=2; 2:r4=1; y=1;
860405:>0:r3=1; 2:r1=0; 2:r4=2; y=2;
293632:>0:r3=1; 2:r1=0; 2:r4=1; y=1;
7673411:>0:r3=1; 2:r1=2; 2:r4=2; y=1;
26547432:>0:r3=1; 2:r1=1; 2:r4=1; y=1;
3273575:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
72491168:>0:r3=1; 2:r1=0; 2:r4=0; y=1;
54765292:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
215641046:>0:r3=0; 2:r1=2; 2:r4=2; y=1;
175081715:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
113232153:>0:r3=0; 2:r1=0; 2:r4=0; y=1;
45463564:>0:r3=0; 2:r1=1; 2:r4=1; y=1;
84106130:>0:r3=1; 2:r1=2; 2:r4=2; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 121.87
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
15954936:>0:r3=1; 2:r1=0; 2:r3=1;
151405658:>0:r3=1; 2:r1=1; 2:r3=1;
233249500:>0:r3=0; 2:r1=0; 2:r3=1;
31040022:>0:r3=1; 2:r1=1; 2:r3=0;
231617711:>0:r3=1; 2:r1=0; 2:r3=0;
103484528:>0:r3=0; 2:r1=0; 2:r3=0;
33247645:>0:r3=0; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 122.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww032 Allowed
Histogram (18 states)
83623 :>0:r3=0; 2:r1=0; 2:r3=1; y=1;
3766442:>0:r3=0; 2:r1=0; 2:r3=2; y=1;
530425:>0:r3=1; 2:r1=2; 2:r3=1; y=1;
972778:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
9584689:>0:r3=0; 2:r1=2; 2:r3=1; y=1;
1172508:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
39946919:>0:r3=0; 2:r1=1; 2:r3=1; y=1;
3948187:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
26283259:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
7303210:>0:r3=1; 2:r1=2; 2:r3=2; y=1;
8365658:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
41325960:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
111030000:>0:r3=0; 2:r1=0; 2:r3=0; y=1;
28340756:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
72440091:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
210903985:>0:r3=0; 2:r1=2; 2:r3=2; y=1;
152811315:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
81190195:>0:r3=1; 2:r1=2; 2:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 119.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
272253496:>1:r1=0; 1:r3=1;
391274635:>1:r1=1; 1:r3=1;
616471869:>1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 1280000000
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 88.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1303089:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1695565:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1221717:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
11079194:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1581126:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
28051939:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
68679316:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
27352402:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
94803915:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
26640255:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
95565440:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
27293184:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
137889860:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
47107828:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
69735170:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 163.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,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 bcsdww035 Allowed
Histogram (42 states)
2442 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
929815:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
407532:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
766965:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
1750696:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2703854:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
670980:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
1831909:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
3809527:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1981975:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1411850:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
4766318:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
542195:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
5653164:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
3571355:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
2786726:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
3329471:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
419446:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1132945:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
780817:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
5608036:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1007256:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
1216406:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
6769917:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
2996620:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
17256807:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
4105130:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
12307931:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
25553477:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
63827164:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
24046004:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
37728944:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
62156469:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
39070636:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
12759424:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
50596808:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
46027165:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
103959161:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
7815643:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
23140329:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
31714320:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
21086371:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 180.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: xor 10,28,28
_litmus_P2_2_: lwzx 30,10,9
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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)
4472064:>0:r3=2; 2:r1=1; 2:r4=2; x=2;
2236225:>0:r3=2; 2:r1=0; 2:r4=2; x=2;
15675486:>0:r3=2; 2:r1=0; 2:r4=0; x=2;
46950050:>0:r3=1; 2:r1=1; 2:r4=2; x=1;
12243331:>0:r3=1; 2:r1=0; 2:r4=1; x=1;
45342693:>0:r3=1; 2:r1=1; 2:r4=2; x=2;
342415:>0:r3=2; 2:r1=0; 2:r4=1; x=2;
92712140:>0:r3=1; 2:r1=0; 2:r4=2; x=2;
60690112:>0:r3=1; 2:r1=0; 2:r4=2; x=1;
129623866:>0:r3=1; 2:r1=0; 2:r4=0; x=1;
148792179:>0:r3=1; 2:r1=1; 2:r4=1; x=1;
125002085:>0:r3=1; 2:r1=0; 2:r4=1; x=2;
115917354:>0:r3=1; 2:r1=0; 2:r4=0; x=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 107.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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)
237259:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
1871553:>0:r3=2; 2:r1=0; 2:r3=2; x=2;
4389776:>0:r3=2; 2:r1=1; 2:r3=2; x=2;
15218844:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
16408200:>0:r3=1; 2:r1=0; 2:r3=1; x=1;
33285110:>0:r3=1; 2:r1=1; 2:r3=2; x=2;
113414502:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
127741600:>0:r3=1; 2:r1=0; 2:r3=1; x=2;
142302263:>0:r3=1; 2:r1=1; 2:r3=1; x=1;
126546627:>0:r3=1; 2:r1=0; 2:r3=0; x=1;
105439873:>0:r3=1; 2:r1=0; 2:r3=2; x=2;
79704087:>0:r3=1; 2:r1=0; 2:r3=2; x=1;
33440306:>0:r3=1; 2:r1=1; 2:r3=2; x=1;
No
Witnesses
Positive: 0, Negative: 800000000
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 109.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 11,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 bcsdww038 Allowed
Histogram (108 states)
3010 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2945 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2059 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
576 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
2130 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
584 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
3957 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
3973 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
19091 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
122221:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
35111 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
14611 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
46473 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
423049:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
180193:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
7765 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
21444 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
14112 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
34634 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
101410:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
68676 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
1299383:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
184253:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
45449 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
33237 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
1215028:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
53694 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
430967:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
154425:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
247453:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
122826:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
20767 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
53491 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
103458:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
224217:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
153247:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
435539:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1289199:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
251104:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
599314:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
223128:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
1268608:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
247587:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
425698:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
67994 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
984855:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
2524939:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
1258987:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2541833:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2473059:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1582538:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
1005758:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1201236:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
836840:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
4552476:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1282503:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
4025622:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
2670829:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
825169:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1570962:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
1423492:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2446336:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
4162506:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
597791:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
4010885:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
982752:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2480506:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
3622050:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
6743540:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
3641218:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
1019223:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1266957:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
6634083:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
2482480:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
2649744:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
997488:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
823447:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
8512201:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
6346632:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
974205:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
2142957:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
11973486:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
17145466:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
11962204:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
6361970:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
2144295:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
12536342:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
38411812:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
40016641:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
250390:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
17085816:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
12452722:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
40052716:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
1437038:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
40230993:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
38402911:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
8511551:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
837093:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1454116:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
6541203:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
46556657:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
12551133:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
4163856:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
46528249:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
6754003:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
40208652:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
4538780:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
67333716:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 232.57
$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: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=-s 4000
Thu Dec 31 16:29:45 GMT 2009