Fri Jan 1 18:02:05 CET 2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
Test bclwdww000 Allowed
Histogram (3 states)
26924095:>1:r1=0; x=1;
78005803:>1:r1=0; x=2;
55070102:>1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 160000000
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 100.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: li r8,1
_litmus_P3_3_: stwx r8,r11,r2
Test bclwdww001 Allowed
Histogram (15 states)
8460 :>1:r1=1; 3:r1=1; x=2; z=1;
36058 :>1:r1=0; 3:r1=1; x=2; z=2;
5064 :>1:r1=1; 3:r1=1; x=1; z=2;
23359 :>1:r1=1; 3:r1=0; x=2; z=2;
2252217:>1:r1=0; 3:r1=1; x=1; z=2;
1117728:>1:r1=1; 3:r1=0; x=1; z=2;
2517477:>1:r1=1; 3:r1=0; x=2; z=1;
1939280:>1:r1=0; 3:r1=1; x=2; z=1;
5031548:>1:r1=1; 3:r1=1; x=1; z=1;
12613997:>1:r1=0; 3:r1=1; x=1; z=1;
13096923:>1:r1=0; 3:r1=0; x=1; z=2;
9456103:>1:r1=0; 3:r1=0; x=2; z=2;
15205734:>1:r1=0; 3:r1=0; x=2; z=1;
13288711:>1:r1=1; 3:r1=0; x=1; z=1;
3407341:>1:r1=0; 3:r1=0; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 208.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li r10,1
_litmus_P3_3_: stw r10,0(r2)
Test bclwdww002 Allowed
Histogram (15 states)
3878 :>1:r1=1; 3:r1=1; x=2; z=1;
5541 :>1:r1=1; 3:r1=1; x=1; z=2;
5422 :>1:r1=1; 3:r1=0; x=2; z=2;
37272 :>1:r1=0; 3:r1=1; x=2; z=2;
1107147:>1:r1=1; 3:r1=0; x=1; z=2;
1561771:>1:r1=0; 3:r1=1; x=2; z=1;
1976969:>1:r1=0; 3:r1=1; x=1; z=2;
802552:>1:r1=1; 3:r1=0; x=2; z=1;
12460498:>1:r1=0; 3:r1=1; x=1; z=1;
13429889:>1:r1=0; 3:r1=0; x=1; z=2;
4779033:>1:r1=0; 3:r1=0; x=1; z=1;
9889553:>1:r1=0; 3:r1=0; x=2; z=2;
16108568:>1:r1=0; 3:r1=0; x=2; z=1;
4247204:>1:r1=1; 3:r1=1; x=1; z=1;
13584703:>1:r1=1; 3:r1=0; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 199.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r6,0(r9)
_litmus_P3_1_: xor r11,r6,r6
_litmus_P3_2_: lwzx r7,r11,r2
Test bclwdww003 Allowed
Histogram (15 states)
1928 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
9849 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
4209 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
14186 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
812679:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
3268092:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
1027995:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
2492247:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
4720846:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
15853854:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
12774055:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
15751813:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
7216331:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
11908973:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
4142943:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 187.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww004 Allowed
Histogram (36 states)
5 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
13 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
5 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
27 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
45 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
33 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
50 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
273 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
346 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
200 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
786 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
1303 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
1364 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
239 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
3954 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
698 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
72568 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
142774:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
145695:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
744525:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
130124:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
1223723:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
167627:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
920311:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
1897800:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
1261029:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
7076336:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
13083502:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
7078456:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
14255122:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
9296517:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
5767822:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
1652711:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
7323942:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
4642150:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
3107925:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 254.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww005 Allowed
Histogram (15 states)
13920 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
1942 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
1563 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
12436 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
893891:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
1082784:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
8033963:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
4796133:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
13363812:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
2741093:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
12181286:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
14795197:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
15693656:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
2354341:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
4033983:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 181.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww006 Allowed
Histogram (42 states)
1 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
145 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
3211 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
89 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
10711 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
268 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
96841 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
3057 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
1293 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
510 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
67930 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
918 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
297602:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
8100 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
7045 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
55128 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
143465:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
88570 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
113169:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
48092 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
29896 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
23588 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
73854 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
42329 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
93020 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
203299:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
899882:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1010292:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
101850:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
1884079:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
1034262:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
14085502:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
5386763:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
7727686:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
777212:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
1604011:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
9265403:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
6809800:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
14801043:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
6448716:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
4240141:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
2511227:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 279.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: xor r11,r7,r7
_litmus_P2_2_: li r8,1
_litmus_P2_3_: stwx r8,r11,r2
Test bclwdww007 Allowed
Histogram (7 states)
479724:>2:r1=1; x=1; y=2;
825222:>2:r1=1; x=2; y=1;
957722:>2:r1=0; x=2; y=2;
25944649:>2:r1=0; x=2; y=1;
22861310:>2:r1=0; x=1; y=2;
21908484:>2:r1=1; x=1; y=1;
7022889:>2:r1=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 149.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r10,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li r8,1
_litmus_P2_3_: stw r8,0(r2)
Test bclwdww008 Allowed
Histogram (7 states)
460913:>2:r1=1; x=1; y=2;
814219:>2:r1=1; x=2; y=1;
557074:>2:r1=0; x=2; y=2;
26000724:>2:r1=0; x=2; y=1;
21596503:>2:r1=1; x=1; y=1;
7778228:>2:r1=0; x=1; y=1;
22792339:>2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 150.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r6,0(r9)
_litmus_P2_1_: xor r11,r6,r6
_litmus_P2_2_: lwzx r7,r11,r2
Test bclwdww009 Allowed
Histogram (7 states)
519350:>2:r1=1; 2:r4=0; y=1;
1003502:>2:r1=0; 2:r4=0; y=2;
1049338:>2:r1=1; 2:r4=1; y=2;
24727975:>2:r1=1; 2:r4=1; y=1;
23620325:>2:r1=0; 2:r4=0; y=1;
22171234:>2:r1=0; 2:r4=1; y=2;
6908276:>2:r1=0; 2:r4=1; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 134.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_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r2)
_litmus_P2_1_: xor r11,r7,r7
_litmus_P2_2_: lwzx r9,r11,r2
Test bclwdww010 Allowed
Histogram (18 states)
2 :>2:r1=0; 2:r4=1; x=2; y=1;
21 :>2:r1=1; 2:r4=2; x=1; y=2;
65 :>2:r1=0; 2:r4=2; x=2; y=1;
18 :>2:r1=2; 2:r4=1; x=2; y=1;
546 :>2:r1=2; 2:r4=1; x=1; y=1;
470 :>2:r1=0; 2:r4=2; x=1; y=1;
466 :>2:r1=0; 2:r4=1; x=1; y=2;
6249 :>2:r1=0; 2:r4=2; x=1; y=2;
2222 :>2:r1=0; 2:r4=1; x=1; y=1;
369371:>2:r1=1; 2:r4=1; x=2; y=1;
9103104:>2:r1=1; 2:r4=1; x=1; y=2;
5970662:>2:r1=0; 2:r4=0; x=1; y=2;
4578882:>2:r1=2; 2:r4=2; x=1; y=1;
5479856:>2:r1=0; 2:r4=0; x=2; y=1;
8709203:>2:r1=2; 2:r4=2; x=1; y=2;
2360514:>2:r1=1; 2:r4=1; x=1; y=1;
22574030:>2:r1=2; 2:r4=2; x=2; y=1;
20844319:>2:r1=0; 2:r4=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 158.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test bclwdww011 Allowed
Histogram (7 states)
643938:>2:r1=1; 2:r3=0; y=1;
389486:>2:r1=1; 2:r3=1; y=2;
1512320:>2:r1=0; 2:r3=0; y=2;
7663500:>2:r1=0; 2:r3=1; y=1;
24206498:>2:r1=0; 2:r3=0; y=1;
22935140:>2:r1=1; 2:r3=1; y=1;
22649118:>2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=cf3c12d91d4069a3e06aed8f569c6ba5
Cycle=LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW Rfe
Relax bclwdww011 No BCLwSyncdWW
Safe=Fre Wse LwSyncdWW LwSyncdRR
Time bclwdww011 135.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r11,1
_litmus_P1_4_: stw r11,0(r2)
_litmus_P2_0_: lwz r8,0(r2)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r9,0(r2)
Test bclwdww012 Allowed
Histogram (18 states)
8000 :>2:r1=0; 2:r3=2; x=2; y=1;
233 :>2:r1=0; 2:r3=1; x=2; y=1;
13128 :>2:r1=2; 2:r3=1; x=1; y=1;
1186 :>2:r1=1; 2:r3=2; x=1; y=2;
852 :>2:r1=2; 2:r3=1; x=2; y=1;
330355:>2:r1=1; 2:r3=1; x=2; y=1;
15254 :>2:r1=0; 2:r3=1; x=1; y=2;
53076 :>2:r1=0; 2:r3=2; x=1; y=1;
80351 :>2:r1=0; 2:r3=2; x=1; y=2;
104657:>2:r1=0; 2:r3=1; x=1; y=1;
8212079:>2:r1=1; 2:r3=1; x=1; y=2;
5858180:>2:r1=0; 2:r3=0; x=2; y=1;
6935372:>2:r1=0; 2:r3=0; x=1; y=2;
1974239:>2:r1=1; 2:r3=1; x=1; y=1;
4575909:>2:r1=2; 2:r3=2; x=1; y=1;
7978746:>2:r1=2; 2:r3=2; x=1; y=2;
22552820:>2:r1=2; 2:r3=2; x=2; y=1;
21305563:>2:r1=0; 2:r3=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 159.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
Test bclwdww013 Allowed
Histogram (3 states)
36617546:>1:r1=0; x=1;
67363353:>1:r1=0; x=2;
56019101:>1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 160000000
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 101.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: li r10,1
_litmus_P3_3_: stw r10,0(r2)
Test bclwdww014 Allowed
Histogram (15 states)
4137 :>1:r1=1; 3:r1=1; x=2; z=1;
4124 :>1:r1=1; 3:r1=1; x=1; z=2;
8672 :>1:r1=0; 3:r1=1; x=2; z=2;
5354 :>1:r1=1; 3:r1=0; x=2; z=2;
877391:>1:r1=0; 3:r1=1; x=1; z=2;
1151365:>1:r1=1; 3:r1=0; x=1; z=2;
1442677:>1:r1=0; 3:r1=1; x=2; z=1;
8999404:>1:r1=0; 3:r1=0; x=2; z=2;
896547:>1:r1=1; 3:r1=0; x=2; z=1;
13250421:>1:r1=1; 3:r1=0; x=1; z=1;
4572290:>1:r1=1; 3:r1=1; x=1; z=1;
13230509:>1:r1=0; 3:r1=1; x=1; z=1;
14242654:>1:r1=0; 3:r1=0; x=1; z=2;
5329880:>1:r1=0; 3:r1=0; x=1; z=1;
15984575:>1:r1=0; 3:r1=0; x=2; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 201.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r6,0(r9)
_litmus_P3_1_: xor r11,r6,r6
_litmus_P3_2_: lwzx r7,r11,r2
Test bclwdww015 Allowed
Histogram (15 states)
2998 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
5227 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
3136 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
10696 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
1017794:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
947298:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
1341464:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
8299629:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
14684171:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
16480246:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
6194065:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
14487750:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
1308339:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
3503091:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
11714096:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 182.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww016 Allowed
Histogram (39 states)
1 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
1 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
2 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
2 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
29 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
7 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
7 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
7 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
3 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
61 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
179 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
366 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
204 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
1325 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
460 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
516 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
459 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
1591 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
40583 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
4133 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
66523 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
935766:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
70792 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
117583:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
601673:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
72057 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
951130:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
1398427:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
1605749:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
6480063:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
8153440:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
7013110:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
9769298:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
7181175:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
2589464:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
14308571:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
2865203:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
2749159:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
13020881:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 264.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww017 Allowed
Histogram (15 states)
3890 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
22758 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
5504 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
3622 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1180178:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
1006565:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
1200468:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
5529402:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
10904026:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
13420335:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
16795032:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
15457662:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
8036656:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
2360939:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
4072963:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 182.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww018 Allowed
Histogram (42 states)
2 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
65 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
119 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
116 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
2223 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
7013 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
503 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
60656 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
508 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
4663 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
47108 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
2021 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
58848 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
54372 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
1045 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
105640:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
96442 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
15876 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
56520 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
65807 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
318674:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
68522 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
21312 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
67912 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
17197 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
168374:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
584374:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
667057:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
31681 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
868652:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
1500662:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
6825505:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
14048627:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
1131009:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
7225701:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
14195462:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
7159596:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
10881090:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
6289781:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
2273144:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
2856126:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
2219995:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 260.87
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
Test bclwdww019 Allowed
Histogram (3 states)
30578353:>1:r1=0; 1:r4=1;
73872403:>1:r1=0; 1:r4=0;
55549244:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 160000000
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 78.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r6,0(r9)
_litmus_P3_1_: xor r11,r6,r6
_litmus_P3_2_: lwzx r7,r11,r2
Test bclwdww020 Allowed
Histogram (15 states)
16552 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
27873 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
19603 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
54110 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
1127297:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
1620835:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
2875396:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
8633800:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
2921334:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
3647838:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
13101934:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
12269001:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
14603545:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
13278031:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
5802851:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 164.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww021 Allowed
Histogram (38 states)
3 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
5 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
3 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
7 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
3 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
32 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
31 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
14 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
278 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
820 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
384 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
163 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
1702 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
425 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
116 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
182 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
1969 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
53929 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
126075:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
133755:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
62617 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
912794:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
1342885:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
1604138:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
6204858:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
1510742:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
6538406:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
9667499:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
88182 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
14879436:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
2323598:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
5489566:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
8210872:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
12446010:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
5744762:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
430114:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
2223623:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 231.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww022 Allowed
Histogram (15 states)
31045 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
8150 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
31581 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
1281902:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
3819070:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
1516754:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
2529604:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
8829634:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
5268046:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
13835943:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
12872479:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
15232173:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
2058266:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
12676113:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
9240 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 80000000
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 150.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww023 Allowed
Histogram (42 states)
8 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
80 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
1110 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
128 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
782 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
27137 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
5021 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
603 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
5361 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
22616 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
41732 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
93173 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
540 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
9094 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
130 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
146763:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
16331 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
103824:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
24539 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
5947 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
54645 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
57960 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
104554:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
106013:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
180250:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
671961:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
1919711:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
1099682:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
1167326:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
156129:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
211273:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1960301:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
1182801:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
1922619:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
6105916:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
9079535:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
4856131:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
14743824:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
14041197:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
5308618:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
7377897:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
7186738:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 256.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r2)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r2)
_litmus_P3_1_: xor r11,r7,r7
_litmus_P3_2_: lwzx r9,r11,r2
Test bclwdww024 Allowed
Histogram (69 states)
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
1 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
5 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
8 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
6 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
13 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
18 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
38 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
25 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
31 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
13 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
32 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
41 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
101 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
47 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
63 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
13 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
19 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
111 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
64 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
48 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
90 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
173 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
33 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
154 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
23 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
11 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
209 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
53 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
352 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
17 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
24 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
29 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
52 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
8 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
94 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
169 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
36 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
443 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
133 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
3755 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
35028 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
40694 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
74476 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
517099:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
96302 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
725888:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
1449755:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
4108654:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
445566:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
1163054:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
1622169:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
3743208:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
598958:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
6438701:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
557483:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
6764469:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
5149784:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
1433339:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
918636:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
7155633:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
3465591:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
4890291:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
17188545:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
4155267:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
486800:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
6233276:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
534775:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 363.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r2)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww025 Allowed
Histogram (42 states)
2 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
11 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
5 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
22 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
259 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
303 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
34 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
7 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
357 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
151 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
147 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
441 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
95 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
545 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
65 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
522 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
120 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
390 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
608 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
1690 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
52707 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
49402 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
79657 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
82311 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
847961:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
36611 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
344596:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
1031721:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
1388441:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
5932219:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
2457175:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
2773202:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
1837587:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
3525019:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
14412823:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
6317759:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
11064816:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
12886493:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
8659039:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
6214682:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 246.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r2)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: lwzx r9,r11,r2
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww026 Allowed
Histogram (93 states)
1 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
1 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
3 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
97 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
4 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
3 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
8 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
5 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
35 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
43 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
6 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
29 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
44 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
154 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
6 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
2 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
51 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
30 :>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=0; 3:r3=1; x=1; y=1;
209 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
262 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
2141 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
305 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
4776 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
79 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
31 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
763 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
430 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
637 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
1073 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
220 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
3181 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
370 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
331 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
2502 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
69 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
134 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
294 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
9880 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
41 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
4382 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
1021 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
614 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
1221 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
5991 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
2913 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
10561 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
2533 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
29208 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
14214 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
13394 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
107286:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
29323 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
108 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
60509 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
21244 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
63988 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
31144 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
367239:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
63627 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
220628:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
121423:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
439945:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
413536:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
325180:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
187229:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
171966:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
33271 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
473437:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
728699:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
104553:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
3940582:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
6586227:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
1137653:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
301432:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
998435:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
4706126:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
5606956:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
684310:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
1383005:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
6752434:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
4097181:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
1184534:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
17991925:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
3273946:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
5997628:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
7231250:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
4047724:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 450.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
Test bclwdww027 Allowed
Histogram (3 states)
22763702:>1:r1=0; 1:r3=1;
76610705:>1:r1=0; 1:r3=0;
60625593:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 160000000
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 78.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test bclwdww028 Allowed
Histogram (15 states)
8993 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
9430 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
42233 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1524041:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
29422 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1179592:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
2630290:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
12680691:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
4960188:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
12835844:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
14935961:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
13575662:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
8531562:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2863369:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
4192722:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 150.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww029 Allowed
Histogram (42 states)
44 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1063 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
7 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
158 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
3851 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
578 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
177 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
435 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
845 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
11444 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
28362 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
5426 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
67083 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
21208 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
118277:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
7439 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
86343 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
55544 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
64722 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1239693:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
35834 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
165803:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
151775:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
156598:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
234265:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
27924 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
56649 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
1211772:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
142707:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
554629:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
1623420:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1440238:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
8334044:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
7592676:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
5828026:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2623435:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
10322135:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
4990535:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
14071212:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
13276984:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
3275956:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
2170684:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 252.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r11,2
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r2)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r9,0(r2)
_litmus_P2_0_: li r11,2
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r8,0(r2)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r9,0(r2)
Test bclwdww030 Allowed
Histogram (105 states)
3 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
3 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
4 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
4 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
15 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
39 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
16 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
28 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
85 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
30 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
97 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
797 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
29 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
98 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
91 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
251 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
298 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
4984 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
24 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1506 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
293 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
12825 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
218 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
2421 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
163 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
16 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
48 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
45 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
953 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
703 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1610 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
6 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
150 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
13796 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
75989 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
182 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2500 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1965 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
8245 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
5676 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
1192 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
7001 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
50 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
2221 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
6030 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
1264 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
14207 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
225299:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
292 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
1461 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
2779 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
31493 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
9114 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
2277 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
75747 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
12644 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
17017 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
9207 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
9886 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
76584 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
30335 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
26020 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
148744:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
3502 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
55113 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
24388 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
16796 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
163604:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
2579 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
7591 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
15806 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
53517 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
104126:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
28134 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
100377:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
266126:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
31181 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
100865:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
438245:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
105437:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
270053:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
306681:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
325861:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1186003:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
371882:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
96335 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
735028:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
359318:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
4004484:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
1095640:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
340981:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
1204546:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
1255425:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
6390823:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
6545694:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
6866291:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
3657587:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
706430:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
384991:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
3611595:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
4988484:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
17119495:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
4482227:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
6189350:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
5140339:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 492.05
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 80
Fri Jan 1 19:48:55 CET 2010