Wed Dec 23 13:37:34 NFT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww000
"DpdW Wse LwSyncdWW 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 ;
lwsync | 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 30,0(11)
_litmus_P1_1_: xor 31,30,30
_litmus_P1_2_: li 8,1
_litmus_P1_3_: stwx 8,31,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww000 Allowed
Histogram (3 states)
13331660:>1:r1=1; x=1;
15128750:>1:r1=0; x=2;
3539590:>1:r1=0; x=1;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=c704ed5593f60a49b6fe2873fbc99877
Cycle=DpdW Wse LwSyncdWW Rfe
Relax bclwdww000 No BCLwSyncdWW
Safe=Wse DpdW
Time bclwdww000 1.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww001
"DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW 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 ;
lwsync | li r4,1 | lwsync | 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 30,0(11)
_litmus_P3_1_: xor 31,30,30
_litmus_P3_2_: li 8,1
_litmus_P3_3_: stwx 8,31,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 31,30,30
_litmus_P1_2_: li 8,1
_litmus_P1_3_: stwx 8,31,9
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww001 Allowed
Histogram (15 states)
116870:>1:r1=1; 3:r1=1; x=2; z=1;
123596:>1:r1=1; 3:r1=1; x=1; z=2;
28945 :>1:r1=0; 3:r1=0; x=1; z=1;
195651:>1:r1=1; 3:r1=0; x=2; z=2;
186040:>1:r1=0; 3:r1=1; x=2; z=2;
2261343:>1:r1=1; 3:r1=1; x=1; z=1;
1331867:>1:r1=0; 3:r1=1; x=1; z=1;
1217068:>1:r1=1; 3:r1=0; x=1; z=2;
1371611:>1:r1=0; 3:r1=0; x=2; z=1;
1356087:>1:r1=0; 3:r1=0; x=1; z=2;
1144540:>1:r1=0; 3:r1=1; x=2; z=1;
3155076:>1:r1=0; 3:r1=0; x=2; z=2;
1125341:>1:r1=0; 3:r1=1; x=1; z=2;
1095635:>1:r1=1; 3:r1=0; x=2; z=1;
1290330:>1:r1=1; 3:r1=0; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=d6ca5faa9797f1b1addda6b4fc107253
Cycle=DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww001 No BCLwSyncdWW
Safe=Wse DpdW
Time bclwdww001 2.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww002
"LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW 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) | lwsync ;
lwsync | li r4,1 | lwsync | 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 30,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li 31,1
_litmus_P3_3_: stw 31,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 31,30,30
_litmus_P1_2_: li 8,1
_litmus_P1_3_: stwx 8,31,9
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww002 Allowed
Histogram (15 states)
117305:>1:r1=1; 3:r1=1; x=1; z=2;
110292:>1:r1=1; 3:r1=1; x=2; z=1;
136035:>1:r1=1; 3:r1=0; x=2; z=2;
2288835:>1:r1=1; 3:r1=1; x=1; z=1;
169705:>1:r1=0; 3:r1=1; x=2; z=2;
1070348:>1:r1=0; 3:r1=1; x=2; z=1;
1163225:>1:r1=1; 3:r1=0; x=1; z=2;
60223 :>1:r1=0; 3:r1=0; x=1; z=1;
1491105:>1:r1=0; 3:r1=0; x=1; z=2;
992172:>1:r1=1; 3:r1=0; x=2; z=1;
1412924:>1:r1=0; 3:r1=0; x=2; z=1;
1438712:>1:r1=1; 3:r1=0; x=1; z=1;
3033137:>1:r1=0; 3:r1=0; x=2; z=2;
1099127:>1:r1=0; 3:r1=1; x=1; z=2;
1416855:>1:r1=0; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=f222837c1b9c320fc4731d82df04c0c8
Cycle=LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww002 No BCLwSyncdWW
Safe=Wse LwSyncdRW DpdW
Time bclwdww002 2.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww003
"DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW 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 ;
lwsync | li r4,1 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 8,30,30
_litmus_P3_2_: lwzx 31,8,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 31,30,30
_litmus_P1_2_: li 8,1
_litmus_P1_3_: stwx 8,31,9
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww003 Allowed
Histogram (15 states)
141081:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
24412 :>1:r1=0; 3:r1=0; 3:r4=1; z=1;
209985:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
151269:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
136820:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
1105366:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
2246242:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
1115249:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
1291684:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
1017297:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
3279904:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
1270215:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
1423029:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
1251922:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1335525:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=13e9eff5346eb465cffd68e7d2363168
Cycle=DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww003 No BCLwSyncdWW
Safe=Fre Wse DpdW DpdR
Time bclwdww003 2.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww004
"DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW 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 ;
lwsync | li r4,1 | lwsync | 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 31,0(9)
_litmus_P3_1_: xor 8,31,31
_litmus_P3_2_: lwzx 11,8,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 31,30,30
_litmus_P1_2_: li 8,1
_litmus_P1_3_: stwx 8,31,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww004 Allowed
Histogram (41 states)
576 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
13 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
3 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
14 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
619 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
66 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
138 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
37 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
367 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
130 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
679 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
156 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
266 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
249 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
572 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
1491 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
1810 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
89 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
1919 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
634238:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
321552:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
8122 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
163875:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
165332:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
23734 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1370341:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
328647:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
215237:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
752991:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
213485:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
672941:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
105253:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
1065178:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
1491464:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
276249:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
2272487:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
1216836:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
1285741:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
1124889:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1192758:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
1089456:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=819caebc895b4fb2e9c9cb702b8483e8
Cycle=DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww004 No BCLwSyncdWW
Safe=Fre Wse DpsR DpdW
Time bclwdww004 2.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww005
"LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW 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) | lwsync ;
lwsync | li r4,1 | lwsync | 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 30,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 31,30,30
_litmus_P1_2_: li 8,1
_litmus_P1_3_: stwx 8,31,9
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww005 Allowed
Histogram (15 states)
140781:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
128248:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
166540:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
1042953:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
1132227:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
1132765:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
1338783:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
245964:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
1241368:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
1298347:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
2150071:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
1448855:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
1275311:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
27105 :>1:r1=0; 3:r1=0; 3:r3=1; z=1;
3230682:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=1b7673dab67cdeed3a93a9f78642c123
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww005 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRR DpdW
Time bclwdww005 2.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww006
"LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW 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) | lwsync ;
lwsync | li r4,1 | lwsync | 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 31,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 31,30,30
_litmus_P1_2_: li 8,1
_litmus_P1_3_: stwx 8,31,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww006 Allowed
Histogram (41 states)
5 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
1 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
15 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
55 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
10 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
19 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
11 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
83 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
173 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
216 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
25 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
66 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
566 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
64 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
103 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
662 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
43 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
92 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
121 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
65 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
202684:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
142609:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
19935 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
167156:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
1097125:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
600633:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
685973:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
312822:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
259002:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
329977:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
1302623:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
2313237:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
89479 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
211333:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
721773:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
1149456:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
1161667:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
1290275:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
1159822:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
1196283:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
1583741:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=355c23adb39c4f8a03f27206e6d5ad02
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe
Relax bclwdww006 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR DpdW
Time bclwdww006 2.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww007
"DpdW Wse LwSyncdWW Wse LwSyncdWW 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 ;
lwsync | lwsync | 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 30,0(11)
_litmus_P2_1_: xor 31,30,30
_litmus_P2_2_: li 8,1
_litmus_P2_3_: stwx 8,31,9
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 31,2
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww007 Allowed
Histogram (7 states)
235773:>2:r1=0; x=1; y=1;
1689018:>2:r1=1; x=1; y=2;
1752035:>2:r1=1; x=2; y=1;
2226779:>2:r1=0; x=2; y=2;
4786779:>2:r1=1; x=1; y=1;
5160764:>2:r1=0; x=1; y=2;
5148852:>2:r1=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=c71f30898deb2fe2dc12be48ca126717
Cycle=DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww007 No BCLwSyncdWW
Safe=Wse LwSyncdWW DpdW
Time bclwdww007 1.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww008
"LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW 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) | lwsync ;
lwsync | lwsync | 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 30,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 31,2
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww008 Allowed
Histogram (7 states)
1840713:>2:r1=1; x=1; y=2;
1728179:>2:r1=1; x=2; y=1;
5135365:>2:r1=0; x=2; y=1;
4798439:>2:r1=1; x=1; y=1;
5160441:>2:r1=0; x=1; y=2;
316546:>2:r1=0; x=1; y=1;
2020317:>2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=82e869524c51deb209a9e10f0c829a0c
Cycle=LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww008 No BCLwSyncdWW
Safe=Wse LwSyncdWW LwSyncdRW
Time bclwdww008 2.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww009
"DpdR Fre LwSyncdWW Wse LwSyncdWW 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 ;
lwsync | lwsync | 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 29,0(11)
_litmus_P2_1_: xor 8,29,29
_litmus_P2_2_: lwzx 30,8,9
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww009 Allowed
Histogram (7 states)
2227398:>2:r1=0; 2:r4=0; y=2;
1775188:>2:r1=1; 2:r4=1; y=2;
2084211:>2:r1=1; 2:r4=0; y=1;
4462736:>2:r1=1; 2:r4=1; y=1;
4917477:>2:r1=0; 2:r4=1; y=2;
204881:>2:r1=0; 2:r4=1; y=1;
5328109:>2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=2e3c762333e6fd2b122415c163d1229a
Cycle=DpdR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww009 No BCLwSyncdWW
Safe=Fre Wse LwSyncdWW DpdR
Time bclwdww009 1.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww010
"DpsR Fre LwSyncdWW Wse LwSyncdWW 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 ;
lwsync | lwsync | 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 31,0(9)
_litmus_P2_1_: xor 8,31,31
_litmus_P2_2_: lwzx 11,8,9
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_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_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww010 Allowed
Histogram (18 states)
382 :>2:r1=0; 2:r4=2; x=1; y=1;
35 :>2:r1=0; 2:r4=1; x=2; y=1;
172 :>2:r1=1; 2:r4=2; x=1; y=2;
1928 :>2:r1=0; 2:r4=1; x=1; y=1;
1742 :>2:r1=0; 2:r4=2; x=2; y=1;
2829 :>2:r1=0; 2:r4=2; x=1; y=2;
21011 :>2:r1=0; 2:r4=1; x=1; y=2;
14 :>2:r1=2; 2:r4=1; x=1; y=1;
187 :>2:r1=2; 2:r4=1; x=2; y=1;
2065508:>2:r1=1; 2:r4=1; x=2; y=1;
3457122:>2:r1=0; 2:r4=0; x=1; y=2;
2935379:>2:r1=1; 2:r4=1; x=1; y=2;
103687:>2:r1=2; 2:r4=2; x=1; y=1;
677320:>2:r1=1; 2:r4=1; x=1; y=1;
2120063:>2:r1=0; 2:r4=0; x=1; y=1;
4530205:>2:r1=2; 2:r4=2; x=2; y=1;
2193047:>2:r1=0; 2:r4=0; x=2; y=1;
2889369:>2:r1=2; 2:r4=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=3b6264a86335c33f3b93e442e8f4ad38
Cycle=DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww010 No BCLwSyncdWW
Safe=Fre Wse LwSyncdWW DpsR
Time bclwdww010 1.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww011
"LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW 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) | lwsync ;
lwsync | lwsync | 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 30,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww011 Allowed
Histogram (8 states)
1 :>2:r1=1; 2:r3=0; y=2;
2234937:>2:r1=1; 2:r3=0; y=1;
149091:>2:r1=0; 2:r3=1; y=1;
1835152:>2:r1=1; 2:r3=1; y=2;
4306086:>2:r1=1; 2:r3=1; y=1;
2182517:>2:r1=0; 2:r3=0; y=2;
4825697:>2:r1=0; 2:r3=1; y=2;
5466519:>2:r1=0; 2:r3=0; y=1;
Ok
Witnesses
Positive: 1, Negative: 20999999
Condition exists (y=2 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=cf3c12d91d4069a3e06aed8f569c6ba5
Cycle=LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww011 Ok BCLwSyncdWW
Safe=Fre Wse LwSyncdWW LwSyncdRR
Time bclwdww011 2.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww012
"LwSyncsRR Fre LwSyncdWW Wse LwSyncdWW 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) | lwsync ;
lwsync | lwsync | 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 31,0(9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_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_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww012 Allowed
Histogram (18 states)
810 :>2:r1=0; 2:r3=2; x=2; y=1;
181 :>2:r1=0; 2:r3=2; x=1; y=1;
33 :>2:r1=0; 2:r3=1; x=2; y=1;
5 :>2:r1=2; 2:r3=1; x=1; y=1;
1021 :>2:r1=0; 2:r3=2; x=1; y=2;
255 :>2:r1=0; 2:r3=1; x=1; y=1;
188 :>2:r1=1; 2:r3=2; x=1; y=2;
1965 :>2:r1=0; 2:r3=1; x=1; y=2;
190 :>2:r1=2; 2:r3=1; x=2; y=1;
2134060:>2:r1=1; 2:r3=1; x=2; y=1;
100366:>2:r1=2; 2:r3=2; x=1; y=1;
2988873:>2:r1=2; 2:r3=2; x=1; y=2;
698981:>2:r1=1; 2:r3=1; x=1; y=1;
2006572:>2:r1=0; 2:r3=0; x=1; y=1;
3720920:>2:r1=0; 2:r3=0; x=1; y=2;
2017650:>2:r1=0; 2:r3=0; x=2; y=1;
2848173:>2:r1=1; 2:r3=1; x=1; y=2;
4479757:>2:r1=2; 2:r3=2; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=e7d627c7adc87ac2502ce1f2b46f87c5
Cycle=LwSyncsRR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww012 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR LwSyncdWW
Time bclwdww012 1.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww013
"LwSyncdRW Wse LwSyncdWW 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) | lwsync ;
lwsync | 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 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww013 Allowed
Histogram (3 states)
13069155:>1:r1=1; x=1;
4682121:>1:r1=0; x=1;
14248724:>1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=4d1c1648955365c08b4c97b22a8d5408
Cycle=LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww013 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww013 1.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww014
"LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW 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) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | 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 30,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li 31,1
_litmus_P3_3_: stw 31,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww014 Allowed
Histogram (15 states)
130937:>1:r1=1; 3:r1=0; x=2; z=2;
110511:>1:r1=1; 3:r1=1; x=1; z=2;
101620:>1:r1=1; 3:r1=1; x=2; z=1;
163502:>1:r1=0; 3:r1=1; x=2; z=2;
1107400:>1:r1=0; 3:r1=1; x=2; z=1;
1103910:>1:r1=1; 3:r1=0; x=1; z=2;
933745:>1:r1=1; 3:r1=0; x=2; z=1;
92660 :>1:r1=0; 3:r1=0; x=1; z=1;
1538408:>1:r1=0; 3:r1=1; x=1; z=1;
1523714:>1:r1=0; 3:r1=0; x=1; z=2;
2864847:>1:r1=0; 3:r1=0; x=2; z=2;
1530350:>1:r1=1; 3:r1=0; x=1; z=1;
1028599:>1:r1=0; 3:r1=1; x=1; z=2;
1543891:>1:r1=0; 3:r1=0; x=2; z=1;
2225906:>1:r1=1; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=d40b4d76f7e7419bc76f118bb3639055
Cycle=LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww014 No BCLwSyncdWW
Safe=Wse LwSyncdRW
Time bclwdww014 2.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww015
"DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW 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) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r3,1 | lwsync | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 8,30,30
_litmus_P3_2_: lwzx 31,8,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww015 Allowed
Histogram (15 states)
133332:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
147877:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
174297:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
117941:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
992291:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
53917 :>1:r1=0; 3:r1=0; 3:r4=1; z=1;
2205081:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
1067660:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
1387631:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1148932:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
1565311:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
1368472:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
1520748:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
1080280:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
3036230:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=ed6f4c8d626a404d3601d3a343adac19
Cycle=DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww015 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpdR
Time bclwdww015 2.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww016
"DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW 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) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ;
lwsync | li r3,1 | lwsync | 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 31,0(9)
_litmus_P3_1_: xor 8,31,31
_litmus_P3_2_: lwzx 11,8,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww016 Allowed
Histogram (42 states)
2 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
9 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
184 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
65 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
116 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
985 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
81 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
118 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
204 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
2670 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
1420 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
178 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
343 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
400 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
134 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
1054 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
88 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
1540 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
2915 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
1039 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
149648:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
258811:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
7523 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
257835:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
590035:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
218099:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
116332:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
817664:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
1326232:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
1190101:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
1576550:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
657809:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
141759:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
373821:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
52478 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1026629:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
1134343:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
1274934:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
2173503:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
1127934:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
1289775:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
224640:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=cda2e0cac993408d5ce399f8c3bf25da
Cycle=DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww016 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW DpsR
Time bclwdww016 2.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww017
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW 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) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | 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 30,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww017 Allowed
Histogram (15 states)
177132:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
103919:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
150083:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
159507:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
2053686:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
1051146:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
1342186:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
1020492:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
1453841:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
3032946:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
74752 :>1:r1=0; 3:r1=0; 3:r3=1; z=1;
1468134:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
1298300:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
1662151:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
951725:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=bc3782a4ff957f30ebb76bfb73a82170
Cycle=LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww017 No BCLwSyncdWW
Safe=Fre Wse LwSyncdRW LwSyncdRR
Time bclwdww017 2.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww018
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW 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) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | li r3,1 | lwsync | 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 31,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww018 Allowed
Histogram (42 states)
2 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
320 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
144 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
441 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
207 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
80 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
15 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
582 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
54 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
101 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
399 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
1584 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
95 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
187 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
343 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
1650 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
389 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
252672:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
204 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
194 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
643 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
156090:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
1559 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
174372:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
325275:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
295181:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
234836:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
799205:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
552073:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
46486 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
337402:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
151016:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
675284:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
1355730:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
1345989:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
1309827:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
1044508:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
2079507:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
970196:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1585639:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
952426:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
1347093:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=090f9e7edaad20d00811f89adff27ed2
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe
Relax bclwdww018 No BCLwSyncdWW
Safe=Fre Wse LwSyncsRR LwSyncdRW
Time bclwdww018 5.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww019
"DpdR Fre LwSyncdWW 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 ;
lwsync | lwzx r4,r3,r5 ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww019 Allowed
Histogram (3 states)
3424084:>1:r1=0; 1:r4=1;
14542020:>1:r1=0; 1:r4=0;
14033896:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (1:r1=1 /\ 1:r4=0) is NOT validated
Hash=76deedad5ea71bc51dc86d1d5214c15b
Cycle=DpdR Fre LwSyncdWW Rfe
Relax bclwdww019 No BCLwSyncdWW
Safe=Fre DpdR
Time bclwdww019 2.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww020
"DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW 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 ;
lwsync | lwzx r4,r3,r5 | lwsync | 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 8,30,30
_litmus_P3_2_: lwzx 31,8,9
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww020 Allowed
Histogram (15 states)
170874:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
183225:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
181456:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
197297:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
1026127:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
116920:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
1145835:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
1038860:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
1421251:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
1550510:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
1277046:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
1526813:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
2127444:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
2991626:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
1044716:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=95bd88b4aecb95238880fff470fdbcc8
Cycle=DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww020 No BCLwSyncdWW
Safe=Fre DpdR
Time bclwdww020 7.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww021
"DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW 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 ;
lwsync | lwzx r4,r3,r5 | lwsync | 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 31,0(9)
_litmus_P3_1_: xor 8,31,31
_litmus_P3_2_: lwzx 11,8,9
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww021 Allowed
Histogram (43 states)
9 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
3 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
997 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
33 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
6 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
76 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
178 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
165 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
2782 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
183 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
191 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
1860 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
96 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
743 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
118 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
667 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
387 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
2113 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
2735 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
3548 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
965 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
8787 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
307834:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
315903:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
142101:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
189600:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
27085 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
237754:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
223733:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
1174103:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
660751:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
595804:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
86303 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
1326208:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
812852:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
1155457:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
1224585:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
2141798:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
243726:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
1217785:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
1165459:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
1242129:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
1482388:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=26c4ea0f855245b74a15911ba593704d
Cycle=DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww021 No BCLwSyncdWW
Safe=Fre DpsR DpdR
Time bclwdww021 6.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww022
"LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW 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) | lwsync ;
lwsync | lwzx r4,r3,r5 | lwsync | 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 30,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww022 Allowed
Histogram (15 states)
166119:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
153998:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
123077:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
191328:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
196543:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
1536274:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
1096349:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
1368620:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
2093187:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
1053926:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
3186714:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
1090340:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
1255418:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
997908:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
1490199:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=18c468c9529c924b0b9eadcf19d0bf8c
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww022 No BCLwSyncdWW
Safe=Fre LwSyncdRR DpdR
Time bclwdww022 7.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww023
"LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW 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) | lwsync ;
lwsync | lwzx r4,r3,r5 | lwsync | 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 31,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww023 Allowed
Histogram (43 states)
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
12 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
30 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
4 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
39 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
32 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
430 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
405 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
1207 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
161 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1180 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
121 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
633 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
40 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
404 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
407 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
3896 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
184 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
70 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
131 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
345 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
151 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
199885:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
167884:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
203942:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
1459964:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
1264163:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
173689:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
1238617:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
740167:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
636759:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
47380 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
1189034:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
283253:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
156592:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
1051305:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
2328809:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
1231150:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
1103284:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
295674:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
322698:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
625267:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
1270600:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=cc14d1f72457a494131d0111d5791792
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe
Relax bclwdww023 No BCLwSyncdWW
Safe=Fre LwSyncsRR DpdR
Time bclwdww023 5.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww024
"DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW 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 ;
lwsync | lwzx r4,r3,r2 | lwsync | 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 31,0(9)
_litmus_P3_1_: xor 8,31,31
_litmus_P3_2_: lwzx 11,8,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 31,0(9)
_litmus_P1_1_: xor 8,31,31
_litmus_P1_2_: lwzx 11,8,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww024 Allowed
Histogram (90 states)
7 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
4 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
2 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
7 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
4 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
5 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
9 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
3 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
5 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
335 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
87 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
1272 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
25 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
3 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
45 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
81 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
67 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
102 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
27 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
181 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
479 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
50 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=1;
1 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
534 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
1500 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
131 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
72 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
1216 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
104 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
1478 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
51 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
89 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
201 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
1582 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
1103 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
416 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
167 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
341 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
1392 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
219 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
501 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
643 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
1197 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
404 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1155 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
177 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
4053 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
631 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
9001 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
2274 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
1268 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1598 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
4071 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
964 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
629 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
494 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
489 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
2502 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
2512 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
7341 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
319491:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
98584 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
359800:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
301046:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
317281:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
17653 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
296427:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
296619:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
213456:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
690611:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
282782:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
641237:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
284795:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
1352817:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
81203 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
426170:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
405014:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
290393:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
1067689:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
982971:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
1044415:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
230501:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
1277881:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
1043626:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
1155596:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
1397881:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
1068755:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=d9cb89dae7c1c7340715ada64130ec5d
Cycle=DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww024 No BCLwSyncdWW
Safe=Fre DpsR
Time bclwdww024 5.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww025
"LwSyncdRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW 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) | lwsync ;
lwsync | lwzx r4,r3,r2 | lwsync | 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 30,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 31,0(9)
_litmus_P1_1_: xor 8,31,31
_litmus_P1_2_: lwzx 11,8,9
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww025 Allowed
Histogram (43 states)
4 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
7 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
13 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=2;
1660 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
892 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
150 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
704 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
4996 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
86 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
438 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
1363 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
847 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
805 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
3010 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
4945 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
400 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
332 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
835 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
423 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
3524 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
15020 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
6291 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
310034:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
167904:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
45482 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
1011941:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
240703:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
2087013:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
1502846:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
1345723:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
305094:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
268892:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
561550:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
1225858:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
238430:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
277841:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
1207349:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
762856:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
753537:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
1275327:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
1106089:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
205292:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
1053494:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=9e35ea0c011a355376ee19a400e99599
Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww025 No BCLwSyncdWW
Safe=Fre LwSyncdRR DpsR
Time bclwdww025 16.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww026
"LwSyncsRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW 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) | lwsync ;
lwsync | lwzx r4,r3,r2 | lwsync | 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 31,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 31,0(9)
_litmus_P1_1_: xor 8,31,31
_litmus_P1_2_: lwzx 11,8,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww026 Allowed
Histogram (87 states)
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
3 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
5 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
4 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
9 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
26 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
59 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
35 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
34 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
1068 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
965 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
424 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
142 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
11 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
3997 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
33 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
120 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
2258 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1558 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
218 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
314 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
2 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
155 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
175 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
365 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
554 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
437 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
331 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
1542 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
371 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
414 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
863 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
596 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
1797 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
155 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
167 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
1508 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
1620 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
1580 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
79 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
186 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
827 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
126 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
1126 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
638 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
2166 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
2342 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
119 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
339 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
259 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
884 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
2371 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
72 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
3381 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
9744 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
281297:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
318743:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
306146:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
343393:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
313857:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
361895:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
98937 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
213068:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
92853 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
718486:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
263059:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
24192 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
724518:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
328135:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
323525:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
235477:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
1030732:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
1025630:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1311513:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
1087509:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
411025:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
267819:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
971547:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
1093532:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
1378605:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
1337167:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
1088757:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=1d532d0bb6dcdffd3b5563101102cb60
Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe
Relax bclwdww026 No BCLwSyncdWW
Safe=Fre LwSyncsRR DpsR
Time bclwdww026 13.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww027
"LwSyncdRR Fre LwSyncdWW 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) | lwsync ;
lwsync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww027 Allowed
Histogram (3 states)
3216013:>1:r1=0; 1:r3=1;
13923871:>1:r1=1; 1:r3=1;
14860116:>1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=9db44a87c6f0512eb7b557fa626432dc
Cycle=LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww027 No BCLwSyncdWW
Safe=Fre LwSyncdRR
Time bclwdww027 3.92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww028
"LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW 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) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | 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 30,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bclwdww028 Allowed
Histogram (15 states)
211699:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
196829:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
225821:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1473329:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1204737:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
183999:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1507104:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1249520:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
93038 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1370591:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
1303009:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
1965171:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
2971674:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1031205:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1012274:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=55921b82d0e8bcbda1b708c97c7b56b3
Cycle=LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww028 No BCLwSyncdWW
Safe=Fre LwSyncdRR
Time bclwdww028 10.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww029
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW 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) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | lwsync | 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 31,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww029 Allowed
Histogram (43 states)
1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
16 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
7 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
181 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
50 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
24 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
132 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
387 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
445 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
117 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
548 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
114 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
1424 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
717 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
5025 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
256 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
733 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
98 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
1701 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1156 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
106 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
282156:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
314209:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
209060:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
214051:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
185770:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
68726 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
1183215:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
661098:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
1061856:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
1362362:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
763890:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
199091:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
966304:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1283750:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
297325:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
1150069:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
1140238:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1315778:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
969 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
252641:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
2409648:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
664556:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=ed3e4f2d7ea7b66a761b0ef9aadf9b30
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe
Relax bclwdww029 No BCLwSyncdWW
Safe=Fre LwSyncsRR LwSyncdRR
Time bclwdww029 18.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bclwdww030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bclwdww030
"LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW 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) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r2) | lwsync | 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 31,0(9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 31,0(9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 11,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bclwdww030 Allowed
Histogram (91 states)
1 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
2 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
3 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
72 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
4 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
7 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
3 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
27 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
251 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
126 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
7 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
463 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
204 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
19 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
18 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
35 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
930 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
587 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
9 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
1502 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
13 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
953 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
860 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1338 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
2821 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
786 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
132 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
1025 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
142 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
332 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
3157 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
2671 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
197 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
271 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
80 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
414 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
626 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
156 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
70 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
761 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
62 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
118 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
86 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
314 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1072 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
254 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1483 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
1092 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
366 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
155 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
125 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
222 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2203 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
61 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
1067 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2404 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1242 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
397418:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
25597 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
285625:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
317811:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
129519:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
219190:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
424554:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
405783:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
314336:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
211115:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
313047:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1045997:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
299 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
754338:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
412057:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
1320585:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
352735:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
125762:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
857448:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1153773:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
958480:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
385266:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1077055:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1390937:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
639182:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1233770:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
838772:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
376138:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=affa727dfb200dd46b9b0942598eb58d
Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe
Relax bclwdww030 No BCLwSyncdWW
Safe=Fre LwSyncsRR
Time bclwdww030 18.33
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 100000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 10
#endif
#ifndef N_EXE
#define N_EXE (64 < N ? 1 : 64 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread -maix64 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 64 */
GCCOPTS="-Wall -std=gnu99 -O -pthread -maix64"
LITMUSOPTS=
Wed Dec 23 13:40:19 NFT 2009