Thu Dec 24 23:22:45 CET 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_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)
6215393:>1:r1=0; x=1;
19490116:>1:r1=0; x=2;
14294491:>1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 19.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1793 :>1:r1=1; 3:r1=1; x=2; z=1;
1750 :>1:r1=1; 3:r1=1; x=1; z=2;
6275 :>1:r1=0; 3:r1=1; x=2; z=2;
4139 :>1:r1=1; 3:r1=0; x=2; z=2;
274640:>1:r1=1; 3:r1=0; x=1; z=2;
409273:>1:r1=0; 3:r1=1; x=2; z=1;
449694:>1:r1=1; 3:r1=0; x=2; z=1;
2373644:>1:r1=0; 3:r1=0; x=2; z=2;
865019:>1:r1=0; 3:r1=0; x=1; z=1;
508027:>1:r1=0; 3:r1=1; x=1; z=2;
3796197:>1:r1=0; 3:r1=0; x=2; z=1;
3381930:>1:r1=0; 3:r1=1; x=1; z=1;
3370247:>1:r1=0; 3:r1=0; x=1; z=2;
3313472:>1:r1=1; 3:r1=0; x=1; z=1;
1243900:>1:r1=1; 3:r1=1; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 41.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)
941 :>1:r1=1; 3:r1=1; x=1; z=2;
860 :>1:r1=1; 3:r1=1; x=2; z=1;
8574 :>1:r1=0; 3:r1=1; x=2; z=2;
1019 :>1:r1=1; 3:r1=0; x=2; z=2;
551654:>1:r1=0; 3:r1=1; x=1; z=2;
259842:>1:r1=1; 3:r1=0; x=1; z=2;
428451:>1:r1=0; 3:r1=1; x=2; z=1;
211955:>1:r1=1; 3:r1=0; x=2; z=1;
3078921:>1:r1=0; 3:r1=1; x=1; z=1;
3222280:>1:r1=0; 3:r1=0; x=1; z=2;
1080489:>1:r1=0; 3:r1=0; x=1; z=1;
2511073:>1:r1=0; 3:r1=0; x=2; z=2;
3284282:>1:r1=1; 3:r1=0; x=1; z=1;
1194378:>1:r1=1; 3:r1=1; x=1; z=1;
4165281:>1:r1=0; 3:r1=0; x=2; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 42.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3839 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
2265 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
396022:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
11792 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
6856 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
322506:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
830677:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
2211256:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
679021:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
3688929:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
3890944:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
2874767:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
964465:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
1105335:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
3011326:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (40 states)
4 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
2 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
5 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
9 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
5 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
31 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
174 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
144 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
87 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
968 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
10 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
112 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
111 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
81 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
17695 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
106 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
543 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
95952 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
21767 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
301 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
124405:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
218 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
148 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
252163:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
23791 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
337577:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
237 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
136029:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
1039619:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
568781:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
1904760:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
243666:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
3570248:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
1676573:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
3352892:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
1442809:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
443805:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1561751:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
2497665:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
684756:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 56.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4717 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
2263 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
8816 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
426239:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
445258:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
283608:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
533438:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
2141134:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
3059639:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
3893938:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
1162262:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
3503578:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
3404688:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
1127969:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
2453 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 38.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
137 :>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
1958 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
45 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
166 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
20 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
41 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
36298 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
73 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
7214 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
2819 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
2556 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
9839 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
1913 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
9776 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
2960 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
444 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
90580 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
787 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
20776 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
19089 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
11231 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
11277 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
267619:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
82439 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
9543 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
24243 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
181218:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
702243:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
52537 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
872230:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
1329681:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
1934015:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
264338:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
1696583:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
120668:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
3625043:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
1608695:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
526257:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
3270959:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
2656308:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
545381:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 58.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
65969 :>2:r1=1; x=1; y=2;
93378 :>2:r1=1; x=2; y=1;
353444:>2:r1=0; x=2; y=2;
6072845:>2:r1=0; x=1; y=2;
1725945:>2:r1=0; x=1; y=1;
5652637:>2:r1=1; x=1; y=1;
6035782:>2:r1=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 32.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
124623:>2:r1=1; 2:r4=1; y=2;
155185:>2:r1=1; 2:r4=0; y=1;
254666:>2:r1=0; 2:r4=0; y=2;
2238450:>2:r1=0; 2:r4=1; y=1;
5258431:>2:r1=0; 2:r4=1; y=2;
5596215:>2:r1=1; 2:r4=1; y=1;
6372430:>2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 30.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
257468:>2:r1=0; 2:r3=0; y=2;
138046:>2:r1=1; 2:r3=0; y=1;
6361110:>2:r1=0; 2:r3=0; y=1;
2363281:>2:r1=0; 2:r3=1; y=1;
5437917:>2:r1=1; 2:r3=1; y=1;
55842 :>2:r1=1; 2:r3=1; y=2;
5386336:>2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 29.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1866 :>1:r1=0; 3:r1=1; 3:r4=0; z=2;
10193 :>1:r1=1; 3:r1=0; 3:r4=0; z=2;
3028 :>1:r1=1; 3:r1=1; 3:r4=1; z=2;
279491:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
751349:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
390718:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
339310:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
3896535:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
3890768:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
3125547:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
2909780:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
1010103:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
2139646:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
1249029:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
2637 :>1:r1=1; 3:r1=1; 3:r4=0; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 38.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1750 :>1:r1=0; 3:r1=1; 3:r3=0; z=2;
1567 :>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1303 :>1:r1=1; 3:r1=1; 3:r3=1; z=2;
348250:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
236540:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
418054:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
822228:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
3129867:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
1209461:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
12360 :>1:r1=1; 3:r1=0; 3:r3=0; z=2;
3507227:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
3953727:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
2096592:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
1120818:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
3140256:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
7824658:>1:r1=0; 1:r4=1;
18397269:>1:r1=0; 1:r4=0;
13778073:>1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 19.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
15746 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
2952 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
6690 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
3858 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
433252:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
280571:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
861903:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
759538:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
2206103:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
3405138:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
3536120:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
3156974:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
775839:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
3140282:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
1415034:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (42 states)
1 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
2 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
1 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
1 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
9 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
2 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
17 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
9 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
101 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
97 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
92 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
1031 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
73 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
79 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
84 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
86 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
290 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
164 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
72 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
290746:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
56390 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
25048 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
14858 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
195039:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
169 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
51406 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
443325:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
29840 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
1602842:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
2445058:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
1403434:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
3809908:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
2725178:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
479090:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
508500:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
2356093:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
1345194:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
364439:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
1236842:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
614259:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
129 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 55.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2381 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
5523 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
7407 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
3156 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
250276:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
393588:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
3153458:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
467314:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
3942202:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
3167946:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
466690:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
1409473:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
2175847:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
1072922:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
3481817:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (41 states)
140 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
336 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
4 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
106 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
33 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
122 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
13 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
151 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
3464 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
11151 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
752 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
10663 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
3584 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
16281 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
956 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
3980 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
45379 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
23321 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
8466 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
17812 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
19938 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
35179 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
46492 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
11748 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
1259 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
116368:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
478436:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
35467 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1965684:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
510467:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
1897342:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1536811:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
2547550:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
3794225:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
3261856:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
1261695:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
299877:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
289693:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
996461:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
541953:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
204785:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 57.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (37 states)
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
2 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
3 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
2 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
31 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
78 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
57 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
18 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
5 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
63 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
44 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
27 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
504 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
659 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
6 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
196 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
10705 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
228711:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
620714:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
62201 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
67219 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
63736 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
13229 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
22641 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
1333788:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
441861:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
305276:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
1836734:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
3533458:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
616721:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
2772014:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
1549314:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
583235:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
1858362:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
490837:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
3587547:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 52.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
14368105:>1:r1=1; 1:r3=1;
19241732:>1:r1=0; 1:r3=0;
6390163:>1:r1=0; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 19.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1793 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
13435 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
8079 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1664 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
253800:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
375709:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
700307:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
3262082:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
678580:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
3735620:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
3161284:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1238701:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
2021877:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1065252:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
3481817:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 20000000
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 39.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (41 states)
20 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
504 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
27 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
1867 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
27 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
240 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
81 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
117 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
11820 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
1543 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
1007 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
32842 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
15049 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
11253 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
24624 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
4742 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
13177 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
30018 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
290266:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
10719 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
5469 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
49577 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
20418 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
12374 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
271882:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
3650 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
46396 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1464179:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
548666:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1817103:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
414706:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
1903572:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
107523:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
3569155:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
2679513:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
1234740:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
601726:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
3390197:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
847693:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
558336:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
3182 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 54.87
$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: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 20
Thu Dec 24 23:36:49 CET 2009