Fri Jan 1 15:51:41 GMT 2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
196709079:>1:r1=0; x=1;
466153031:>1:r1=1; x=1;
617137890:>1:r1=0; x=2;
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 68.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1247432:>1:r1=1; 3:r1=1; x=2; z=1;
1214497:>1:r1=1; 3:r1=1; x=1; z=2;
2530893:>1:r1=1; 3:r1=0; x=2; z=2;
2957945:>1:r1=0; 3:r1=1; x=2; z=2;
50033410:>1:r1=1; 3:r1=1; x=1; z=1;
28335127:>1:r1=1; 3:r1=0; x=2; z=1;
33458700:>1:r1=0; 3:r1=1; x=1; z=2;
66508351:>1:r1=1; 3:r1=0; x=1; z=1;
91118702:>1:r1=0; 3:r1=0; x=2; z=1;
29193485:>1:r1=0; 3:r1=1; x=2; z=1;
16095408:>1:r1=0; 3:r1=0; x=1; z=1;
121239689:>1:r1=0; 3:r1=0; x=2; z=2;
75397015:>1:r1=0; 3:r1=1; x=1; z=1;
94972831:>1:r1=0; 3:r1=0; x=1; z=2;
25696515:>1:r1=1; 3:r1=0; x=1; 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 161.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
710692:>1:r1=1; 3:r1=1; x=2; z=1;
1264319:>1:r1=1; 3:r1=1; x=1; z=2;
1734981:>1:r1=0; 3:r1=1; x=2; z=2;
1951549:>1:r1=1; 3:r1=0; x=2; z=2;
45555918:>1:r1=1; 3:r1=1; x=1; z=1;
20258668:>1:r1=0; 3:r1=1; x=2; z=1;
27072594:>1:r1=1; 3:r1=0; x=2; z=1;
29333400:>1:r1=0; 3:r1=1; x=1; z=2;
114073398:>1:r1=0; 3:r1=0; x=2; z=2;
21642637:>1:r1=0; 3:r1=0; x=1; z=1;
80268810:>1:r1=1; 3:r1=0; x=1; z=1;
95662012:>1:r1=0; 3:r1=0; x=2; z=1;
68675838:>1:r1=0; 3:r1=1; x=1; z=1;
103830831:>1:r1=0; 3:r1=0; x=1; z=2;
27964353:>1:r1=1; 3:r1=0; x=1; 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 165.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1925316:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
1072248:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
1010558:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
3332562:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
20527614:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
45575181:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
24789236:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
30600264:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
15747599:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
93392256:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
97839203:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
128887526:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
77153418:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
62289920:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
35857099:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
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 156.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
34 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
9158 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
13841 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
35854 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
59200 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
8248 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
142807:>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
209609:>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
39189 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
67233 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
33734 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
82684 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
334684:>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
44395 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
3729236:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
58490 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
32468 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
7403178:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
8167131:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
66453 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
263903:>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
672266:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
132770:>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
3255645:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
12918800:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
1271051:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
742852:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
34898591:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
28313039:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
5355518:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
22635065:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
30379865:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
66826143:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
14271626:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
36867778:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
26974795:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
51082438:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
6813188:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
65003367:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
60318759:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
46798920:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
103665995:>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 168.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1581397:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
2411942:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
2248112:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
1125174:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
16405668:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
30669218:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
29785483:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
25722450:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
88758847:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
99325595:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
77666204:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
118783791:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
65367258:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
30051330:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
50097531:>1:r1=1; 3:r1=1; 3:r3=1; 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 154.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1897 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
837198:>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
478707:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
573698:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
1192589:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
3262911:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
1271548:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1001499:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
5022535:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
2532108:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
1142491:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
10054802:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
1758394:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
681150:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
667922:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
6936971:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
2753425:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
20156869:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
1026166:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
2541541:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
27000153:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
4983540:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
560824:>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
3285463:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
56769522:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
10922806:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
12346488:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
13376324:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
65606916:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
31688670:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
26605266:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
2330709:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
6436631:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
6244622:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3746802:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
97497197:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
41952116:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
34570615:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
28889261:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
57526875:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
38956114:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
4808665:>1:r1=0; 3:r1=1; 3:r3=1; y=2; 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 170.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
27521546:>2:r1=1; x=1; y=2;
31772966:>2:r1=1; x=2; y=1;
53059978:>2:r1=0; x=1; y=1;
65193193:>2:r1=0; x=2; y=2;
208094689:>2:r1=0; x=1; y=2;
245262923:>2:r1=0; x=2; y=1;
169094705:>2:r1=1; x=1; y=1;
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 107.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
21511510:>2:r1=1; x=1; y=2;
20592093:>2:r1=1; x=2; y=1;
153676154:>2:r1=1; x=1; y=1;
253009052:>2:r1=0; x=2; y=1;
78291666:>2:r1=0; x=1; y=1;
228477176:>2:r1=0; x=1; y=2;
44442349:>2:r1=0; x=2; 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 104.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
59343467:>2:r1=0; 2:r4=0; y=2;
20019944:>2:r1=1; 2:r4=1; y=2;
20900247:>2:r1=1; 2:r4=0; y=1;
61609666:>2:r1=0; 2:r4=1; y=1;
289750548:>2:r1=0; 2:r4=0; y=1;
137168696:>2:r1=1; 2:r4=1; y=1;
211207432:>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 99.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1216 :>2:r1=0; 2:r4=1; x=2; y=1;
391535:>2:r1=0; 2:r4=2; x=1; y=1;
371742:>2:r1=2; 2:r4=1; x=2; y=1;
214519:>2:r1=0; 2:r4=1; x=1; y=1;
79334 :>2:r1=2; 2:r4=1; x=1; y=1;
64488 :>2:r1=0; 2:r4=2; x=2; y=1;
90056 :>2:r1=1; 2:r4=2; x=1; y=2;
813109:>2:r1=0; 2:r4=2; x=1; y=2;
1621832:>2:r1=0; 2:r4=1; x=1; y=2;
83002135:>2:r1=2; 2:r4=2; x=1; y=2;
27999082:>2:r1=2; 2:r4=2; x=1; y=1;
67217153:>2:r1=0; 2:r4=0; x=2; y=1;
133996041:>2:r1=0; 2:r4=0; x=1; y=2;
74893231:>2:r1=1; 2:r4=1; x=1; y=2;
192028283:>2:r1=2; 2:r4=2; x=2; y=1;
134605873:>2:r1=0; 2:r4=0; x=1; y=1;
23785066:>2:r1=1; 2:r4=1; x=2; y=1;
58825305:>2:r1=1; 2:r4=1; x=1; y=1;
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 106.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
21486797:>2:r1=1; 2:r3=0; y=1;
20829353:>2:r1=1; 2:r3=1; y=2;
61978306:>2:r1=0; 2:r3=1; y=1;
285475554:>2:r1=0; 2:r3=0; y=1;
139933790:>2:r1=1; 2:r3=1; y=1;
215700440:>2:r1=0; 2:r3=1; y=2;
54595760:>2:r1=0; 2:r3=0; y=2;
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 103.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
30939 :>2:r1=0; 2:r3=1; x=2; y=1;
2502315:>2:r1=2; 2:r3=1; x=1; y=1;
2978046:>2:r1=0; 2:r3=2; x=2; y=1;
1742868:>2:r1=0; 2:r3=1; x=1; y=1;
1435148:>2:r1=0; 2:r3=2; x=1; y=1;
21691434:>2:r1=1; 2:r3=1; x=2; y=1;
4809102:>2:r1=1; 2:r3=2; x=1; y=2;
7812250:>2:r1=2; 2:r3=1; x=2; y=1;
8375856:>2:r1=0; 2:r3=2; x=1; y=2;
16028460:>2:r1=0; 2:r3=1; x=1; y=2;
63330398:>2:r1=0; 2:r3=0; x=2; y=1;
138859005:>2:r1=0; 2:r3=0; x=1; y=2;
25618270:>2:r1=2; 2:r3=2; x=1; y=1;
53118356:>2:r1=1; 2:r3=1; x=1; y=2;
77893538:>2:r1=2; 2:r3=2; x=1; y=2;
128794884:>2:r1=0; 2:r3=0; x=1; y=1;
59334306:>2:r1=1; 2:r3=1; x=1; y=1;
185644825:>2:r1=2; 2:r3=2; x=2; y=1;
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 110.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
418763154:>1:r1=0; x=1;
551311893:>1:r1=0; x=2;
309924953:>1:r1=1; x=1;
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 71.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1092447:>1:r1=0; 3:r1=1; x=2; z=2;
729917:>1:r1=1; 3:r1=1; x=1; z=2;
1245480:>1:r1=1; 3:r1=0; x=2; z=2;
711796:>1:r1=1; 3:r1=1; x=2; z=1;
21293808:>1:r1=1; 3:r1=0; x=1; z=2;
20586606:>1:r1=0; 3:r1=1; x=2; z=1;
22869203:>1:r1=0; 3:r1=1; x=1; z=2;
24772251:>1:r1=1; 3:r1=0; x=2; z=1;
104105456:>1:r1=0; 3:r1=0; x=2; z=2;
40185045:>1:r1=1; 3:r1=1; x=1; z=1;
79277277:>1:r1=0; 3:r1=1; x=1; z=1;
80428609:>1:r1=1; 3:r1=0; x=1; z=1;
107324277:>1:r1=0; 3:r1=0; x=2; z=1;
30326118:>1:r1=0; 3:r1=0; x=1; z=1;
105051710:>1:r1=0; 3:r1=0; x=1; z=2;
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 162.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
729042:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
2076603:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
1409797:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
1210495:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
28161055:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
25172377:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
45261184:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
84961036:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
93924679:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
21263961:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
115832293:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
17945061:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
31726785:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
105364137:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
64961495:>1:r1=1; 3:r1=0; 3:r4=1; 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 153.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
46 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
12456 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
8375 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
5589 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
34941 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
27129 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
29161 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
78913 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
116535:>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
257748:>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
43075 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
60089 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
107765:>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
146607:>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
389216:>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
23912 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
3494215:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
618959:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
71184 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
4738455:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
66418 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
10087651:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
18473719:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
681303:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
604756:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
2050441:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
5474944:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
21247109:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
50963445:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
43157 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
20529061:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
24205622:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
31343925:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
101983197:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
11736965:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
73275303:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
57333246:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
6174448:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
37127798:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
31827635:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
54021806:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
70483681:>1:r1=0; 3:r1=0; 3:r4=0; 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 168.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
814676:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
1617972:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
1283044:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
1038985:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
41255127:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
25351503:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
25567885:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
19283471:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
26141803:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
25998376:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
72159028:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
76907820:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
114583353:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
109977538:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
98019419:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
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 156.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1927 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
703991:>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
637184:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
3148783:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
4184190:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
1344492:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
404879:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
332569:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
429789:>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
5629574:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
1574217:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
962570:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
1067683:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
1869436:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
1326925:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
3059831:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
2197727:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
13313933:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
7803497:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
5718386:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
3813346:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
19506889:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
3381631:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
10882496:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
27454030:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
29559717:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
560620:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
4231643:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
4933365:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
1017847:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
1410080:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
18867081:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
45588951:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
11855574:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
37507427:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
55042890:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
67398273:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
22200037:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
65089927:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
40224014:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
96114839:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
17647740:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
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 165.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
299517388:>1:r1=0; 1:r4=1;
349389207:>1:r1=1; 1:r4=1;
631093405:>1:r1=0; 1:r4=0;
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 67.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1504254:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
1631711:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
2951962:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
2820016:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
27545205:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
32158004:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
12787163:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
53498537:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
69492255:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
67324394:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
91852604:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
93663559:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
29663878:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
122198881:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
30907577:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
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 149.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6420 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
40261 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
104 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
11290 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
373130:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
64919 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
43742 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
8505 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
228095:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
28345 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
41379 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
95694 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
92674 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
3531535:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
135785:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
3432743:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
6290053:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
7657782:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
12678558:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
29133325:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
168096:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
6156533:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
267262:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
81556 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
51510 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
919855:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
44272 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
917308:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
47493519:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
28070602:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
36027094:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
13838960:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
27697493:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
58483907:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
5957577:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
71230887:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
45445292:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
21687516:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
108253553:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
1282751:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
69206034:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
32824084:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; 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 165.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1549834:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
2544375:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
2394858:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
1194061:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
48907516:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
27924880:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
24450779:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
31575704:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
63117098:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
75289967:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
121703246:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
97654411:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
16199387:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
95259335:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
30234549:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
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 150.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2224 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
3190547:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
720674:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
1156329:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
586430:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
782833:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
515498:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
1123285:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
986918:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
555986:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
2323033:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
1046021:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
5430607:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1516948:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
2615413:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
13078489:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
3841872:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
10307641:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
1272757:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
6220716:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
11415522:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
2158596:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
6567810:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
2813499:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
56609101:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
35934476:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
4069948:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
13751914:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
5485777:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
27400174:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
5912624:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
19752723:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
26388403:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
1656709:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
61420898:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
32633936:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
40478978:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
27558809:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
3287336:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
65379446:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
101809818:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
30239282:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
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 166.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (104 states)
5 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
8 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
7 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
10 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
88 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
74 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
52 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
23 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
23 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
80 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
87 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
16 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
36 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
39 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
130 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
100 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
695 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
747 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
116 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
210 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
123 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
126 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
83 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
170 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
6 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
12882 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
53252 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
12404 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
568 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
120288:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
8100 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
97478 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
26440 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
13827 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
27569 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
5790 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
12693 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
15462 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
22566 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
32062 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
40140 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
79418 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
107404:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
26636 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
5465 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
102235:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
99650 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
134000:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
23520 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
77731 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
47034 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
623 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=1;
77 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
23017 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
90543 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
23180 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
56245 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
52274 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
175034:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
8250 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
151484:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
38412 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
122073:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
23411 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
74806 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
12574 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
351563:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
187762:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
552313:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
55104 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
53503 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
45439 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
372942:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
26991 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
546131:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
158356:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
4099273:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
15176914:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
2311716:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
8644487:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
4172388:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
3376154:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
8344792:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
7337264:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
50883215:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
7958092:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
7508077:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
43642458:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
3362182:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
12842967:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
12841439:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
43577830:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
18018503:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
17677649:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
38773323:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
19663923:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
54287345:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
80183379:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
7476714:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
19317689:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
54320933:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
50791856:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
38999659:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; 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: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 216.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
75 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
36486 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
8591 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
37636 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
62911 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
26375 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
112323:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
79438 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
7612 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
68773 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
39346 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
14640 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
249494:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
672507:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
335079:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
38136 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
55248 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
140485:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
26879 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
183623:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
631584:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
2668025:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
890272:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
17864500:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
3494258:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
32245800:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
7105476:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
10657104:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
4698616:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
22201535:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
6185958:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
21535107:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
49699697:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
79037221:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
23804826:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
54669952:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
108475666:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
65940863:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
32597319:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
9495614:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
31289198:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
52615752:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
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 159.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
9 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
22 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
7 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
24 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
133 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
41 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
75 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
1259 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
734 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1250 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
1992 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
5445 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
544 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
1222 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
23450 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
141 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
1588 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
6443 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
675 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
652 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
234 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
5522 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
926 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
9445 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
1368 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
1605 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
4492 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
2747 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
5490 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
17192 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
7472 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
39881 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
5353 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
13201 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
105441:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
1164 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
36358 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
66490 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
23919 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
117859:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
21198 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
37879 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
179355:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
16989 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
11646 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
132451:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
1552149:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
43848 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
55985 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
27619 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
96423 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
78860 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
11878 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
209714:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
298668:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
66527 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
359567:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
904404:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
1141420:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
317834:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
493537:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
1397674:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
1547518:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
5797031:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
433934:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
837445:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
22620 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
3003092:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
1281171:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
2165642:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
615660:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
1082795:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
2912995:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
1502139:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
1446457:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
1029727:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
3005374:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
2759721:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
4346662:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
847322:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
2008238:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
48612424:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
7598727:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
9778903:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
3702768:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
3873336:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
2681419:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
6785577:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
37863712:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
17255380:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
13923681:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
48463356:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
10409837:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
7110686:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
36784001:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
5668517:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
54547772:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
7478706:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
17284089:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
8086469:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
41355645:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
37933615:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
4155859:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
78291932:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
16354723:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
39364114:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
10294515:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
19727204:>1:r1=2; 1:r4=2; 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: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 212.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
38587272:>0:r3=1; 2:r1=0; x=1;
100596827:>0:r3=0; 2:r1=0; x=2;
31615286:>0:r3=1; 2:r1=1; x=2;
227523814:>0:r3=0; 2:r1=0; x=1;
211796536:>0:r3=1; 2:r1=0; x=2;
152052628:>0:r3=1; 2:r1=1; x=1;
37827637:>0:r3=0; 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 99.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
21003513:>0:r3=1; 2:r1=1; x=2;
141897608:>0:r3=1; 2:r1=1; x=1;
30584812:>0:r3=0; 2:r1=1; x=1;
74658972:>0:r3=0; 2:r1=0; x=2;
57555853:>0:r3=1; 2:r1=0; x=1;
252799895:>0:r3=0; 2:r1=0; x=1;
221499347:>0:r3=1; 2:r1=0; 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 102.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
41041581:>0:r3=0; 2:r1=1; 2:r4=1;
96008846:>0:r3=0; 2:r1=0; 2:r4=0;
155081979:>0:r3=1; 2:r1=1; 2:r4=1;
29122234:>0:r3=1; 2:r1=0; 2:r4=1;
220270849:>0:r3=0; 2:r1=0; 2:r4=1;
221889316:>0:r3=1; 2:r1=0; 2:r4=0;
36585195:>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 97.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
8088 :>0:r3=1; 2:r1=2; 2:r4=1; y=1;
3964 :>0:r3=0; 2:r1=0; 2:r4=1; y=1;
13899 :>0:r3=1; 2:r1=1; 2:r4=2; y=2;
59879 :>0:r3=0; 2:r1=0; 2:r4=2; y=1;
257879:>0:r3=0; 2:r1=2; 2:r4=1; y=1;
320938:>0:r3=1; 2:r1=0; 2:r4=2; y=1;
328182:>0:r3=1; 2:r1=0; 2:r4=1; y=1;
640579:>0:r3=1; 2:r1=0; 2:r4=2; y=2;
1794232:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
30432639:>0:r3=0; 2:r1=1; 2:r4=1; y=1;
69750220:>0:r3=1; 2:r1=2; 2:r4=2; y=2;
17302536:>0:r3=1; 2:r1=2; 2:r4=2; y=1;
175707073:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
51211841:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
82210638:>0:r3=1; 2:r1=0; 2:r4=0; y=1;
35987227:>0:r3=1; 2:r1=1; 2:r4=1; y=1;
222809683:>0:r3=0; 2:r1=2; 2:r4=2; y=1;
111160503:>0:r3=0; 2:r1=0; 2:r4=0; y=1;
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 108.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
34139453:>0:r3=0; 2:r1=1; 2:r3=1;
24189634:>0:r3=1; 2:r1=1; 2:r3=0;
134039393:>0:r3=1; 2:r1=1; 2:r3=1;
41384287:>0:r3=1; 2:r1=0; 2:r3=1;
242189969:>0:r3=1; 2:r1=0; 2:r3=0;
232275824:>0:r3=0; 2:r1=0; 2:r3=1;
91781440:>0:r3=0; 2:r1=0; 2:r3=0;
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 98.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
70241 :>0:r3=0; 2:r1=0; 2:r3=1; y=1;
1843337:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
4675047:>0:r3=0; 2:r1=0; 2:r3=2; y=1;
1549427:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
1187979:>0:r3=1; 2:r1=2; 2:r3=1; y=1;
8672238:>0:r3=0; 2:r1=2; 2:r3=1; y=1;
21717011:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
10202158:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
35007381:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
4021449:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
74593133:>0:r3=1; 2:r1=2; 2:r3=2; y=2;
26791384:>0:r3=0; 2:r1=1; 2:r3=1; y=1;
40519922:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
99006636:>0:r3=0; 2:r1=0; 2:r3=0; y=1;
14652772:>0:r3=1; 2:r1=2; 2:r3=2; y=1;
149738530:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
91649226:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
214102129:>0:r3=0; 2:r1=2; 2:r3=2; y=1;
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 108.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
325042704:>1:r1=1; 1:r3=1;
337987191:>1:r1=0; 1:r3=1;
616970105:>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 67.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1089360:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
22500708:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1804531:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1094603:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1719335:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
26947318:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
71938886:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
120914819:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
24314052:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
102228271:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
24442873:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
102907593:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
70906805:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
26246945:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
40943901:>1:r1=1; 1:r3=1; 3:r1=1; 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 146.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
470991:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
2794400:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
674326:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
876536:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
962877:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
1069752:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1429602:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
434127:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
1240184:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
460143:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1766 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
2827747:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
1525672:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2003861:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
3881368:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
794837:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
5634339:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
7948835:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
3380223:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
3378683:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1226495:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
2025324:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
4701197:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
26689147:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
16614659:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
5439417:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
13739389:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
8848183:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
32494515:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
5085204:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
19340691:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
36561978:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
22708989:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
66596853:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1876405:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
21952439:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
51925579:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
43346618:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
105976929:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
69441488:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
30011188:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
11607044:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 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 167.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
31092831:>0:r3=1; 2:r1=1; 2:r4=2; x=1;
547059:>0:r3=2; 2:r1=0; 2:r4=1; x=2;
3390165:>0:r3=2; 2:r1=1; 2:r4=2; x=2;
43461520:>0:r3=1; 2:r1=1; 2:r4=2; x=2;
13981771:>0:r3=2; 2:r1=0; 2:r4=0; x=2;
142781976:>0:r3=1; 2:r1=1; 2:r4=1; x=1;
128939505:>0:r3=1; 2:r1=0; 2:r4=0; x=1;
3833809:>0:r3=2; 2:r1=0; 2:r4=2; x=2;
105398459:>0:r3=1; 2:r1=0; 2:r4=1; x=2;
33437019:>0:r3=1; 2:r1=0; 2:r4=1; x=1;
61888335:>0:r3=1; 2:r1=0; 2:r4=2; x=1;
116957160:>0:r3=1; 2:r1=0; 2:r4=0; x=2;
114290391:>0:r3=1; 2:r1=0; 2:r4=2; 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 97.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4233213:>0:r3=2; 2:r1=1; 2:r3=2; x=2;
3923914:>0:r3=2; 2:r1=0; 2:r3=2; x=2;
435030:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
26495049:>0:r3=1; 2:r1=1; 2:r3=2; x=1;
37354050:>0:r3=1; 2:r1=1; 2:r3=2; x=2;
15817688:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
127535806:>0:r3=1; 2:r1=1; 2:r3=1; x=1;
114457261:>0:r3=1; 2:r1=0; 2:r3=2; x=2;
78506679:>0:r3=1; 2:r1=0; 2:r3=2; x=1;
125576266:>0:r3=1; 2:r1=0; 2:r3=0; x=1;
41902730:>0:r3=1; 2:r1=0; 2:r3=1; x=1;
115726993:>0:r3=1; 2:r1=0; 2:r3=1; x=2;
108035321:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
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 96.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
349 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
1466 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
339 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1109 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1267 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
3023 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
6097 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
58361 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
9051 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1138 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
110817:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
3017 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
43810 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
47031 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
18803 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
110286:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
57602 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
171258:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
242273:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
93288 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
54415 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
678108:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
785973:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
56686 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
9067 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
953396:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
827342:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1345325:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
331374:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
58620 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1193881:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1233396:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
2151323:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1012779:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
18435 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
400193:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
122112:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
3456238:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
46178 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
1012170:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
30883 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1119959:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
11893046:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
83864 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
796676:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
5176489:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
220120:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
1946120:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
305862:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
737986:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1318691:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
281981:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
22427 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
811136:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
102227:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
2674179:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
383674:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
2327415:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2193964:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
2769955:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
930739:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
645364:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1385255:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
7588485:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
183273:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
401426:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
7674116:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
7931231:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
15822062:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
823098:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
604240:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1723845:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
2412313:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
3403880:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
1928494:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
3845992:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
279043:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
1655336:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
4179927:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
715634:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
39060533:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
5729051:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
409119:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
5295007:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
9481378:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
1278438:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
1042012:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
5594687:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
3719316:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
1203282:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
9737695:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
16921843:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
1400297:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
4269310:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
3914628:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
2477836:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
50385005:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
16770708:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
16168336:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
38135623:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
76123674:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
3754009:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
38808610:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
38676233:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
38325698:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
7879452:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
49805000:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
37575417:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; 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 215.56
$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 80000 -r 1000
Fri Jan 1 17:19:15 GMT 2010