Wed Dec 23 13:46:22 NFT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr000
"Fre SyncdWW Rfe PodRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) ;
sync | ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test podrr000 Allowed
Histogram (3 states)
4932037:>1:r1=0; 1:r3=1;
15661396:>1:r1=0; 1:r3=0;
11406567:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=78d7a77bf8b1a9bd43cfddf06e35d5d3
Cycle=Fre SyncdWW Rfe PodRR
Relax podrr000 No PodRR
Safe=Fre BCSyncdWW
Time podrr000 1.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr001
"Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwz 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test podrr001 Allowed
Histogram (15 states)
120245:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
126250:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1140779:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
209366:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1284128:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1192325:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
176738:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
996339:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1595443:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
928123:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
77086 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1733004:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
1273665:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
3566580:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1579929:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=2e6b2a124722ed948c8f7dc35dc4b80f
Cycle=Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr001 No PodRR
Safe=Fre BCSyncdWW
Time podrr001 2.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr002
"Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: li 4,1
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwz 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr002 Allowed
Histogram (33 states)
10847 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1803 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
34126 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
50500 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
41705 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
102456:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
55695 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
206195:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
84697 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
59364 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
86177 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
227976:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
151055:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
120444:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
5094 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
75400 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
252080:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
1097573:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
751899:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
168359:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
174023:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
363934:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
83984 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
643757:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1099866:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1946647:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1273634:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
17898 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
3221042:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
901861:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
115139:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1210257:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1364513:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c594109cf9f75c58c9eec5a696ceb0a0
Cycle=Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr002 No PodRR
Safe=Fre BCSyncsWW BCSyncdWW
Time podrr002 2.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr003
"Fre SyncdWW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,1 | ;
li r3,1 | stw r3,0(r4) | ;
stw r3,0(r4) | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test podrr003 Allowed
Histogram (7 states)
556214:>1:r1=0; 2:r1=0; 2:r3=1;
2093472:>1:r1=0; 2:r1=1; 2:r3=0;
1263451:>1:r1=1; 2:r1=1; 2:r3=1;
6102399:>1:r1=0; 2:r1=0; 2:r3=0;
4692593:>1:r1=0; 2:r1=1; 2:r3=1;
4464577:>1:r1=1; 2:r1=0; 2:r3=1;
1827294:>1:r1=1; 2:r1=0; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=3d48b5b0d8516d3d909b0a4f66959c71
Cycle=Fre SyncdWW Rfe SyncdRW Rfe PodRR
Relax podrr003 No PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr003 1.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr004
"Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,1 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test podrr004 Allowed
Histogram (15 states)
153832:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
64150 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
139344:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
110829:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
818432:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
811061:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
137985:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1375451:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
1607683:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
1418101:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
2960817:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
1808905:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
1074344:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
2206403:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
1312663:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=b2067185c885838837d33372d57790fb
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr004 No PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr004 2.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr005
"Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,1 | ;
li r3,2 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r2) | | | ;
exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr005 Allowed
Histogram (33 states)
439 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
14686 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
8743 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
43886 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
47974 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
14007 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
46751 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
41313 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
48911 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
34401 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
23000 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
116992:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
81123 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
78846 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
160180:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
143570:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
705637:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
125537:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
222830:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
200076:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
906147:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
140636:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
1157844:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
957281:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
127361:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
2654709:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
253938:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
2531089:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
862878:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1279470:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
56809 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
1538193:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1374743:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=1a4d6f8ada041391fb8c242b28f54910
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr005 No PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr005 2.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr006
"Fre SyncsWW Rfe SyncdRW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,1 | ;
li r3,2 | stw r3,0(r4) | ;
stw r3,0(r2) | | ;
exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr006 Allowed
Histogram (15 states)
276119:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
24348 :>1:r1=1; 2:r1=1; 2:r3=1; y=2;
89244 :>1:r1=1; 2:r1=0; 2:r3=2; y=2;
211672:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
30071 :>1:r1=0; 2:r1=0; 2:r3=1; y=2;
246889:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
143715:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
388328:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
431293:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
1946362:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
3408756:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
2000660:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
4769755:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
2721985:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
4310803:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=f5e5097c67500c52603a1c0158bb8551
Cycle=Fre SyncsWW Rfe SyncdRW Rfe PodRR
Relax podrr006 No PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr006 1.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr007
"Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,2 | li r3,1 | ;
li r3,1 | stw r3,0(r2) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 10,2
_litmus_P1_3_: stw 10,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test podrr007 Allowed
Histogram (31 states)
124343:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
24171 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
227487:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
125576:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
23594 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
294584:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
310858:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
62850 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
146452:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
936122:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
126539:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
423795:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
541928:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
1258347:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
148062:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
237302:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
1253547:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
163864:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
1084065:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
666327:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
74263 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
64796 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
109191:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
1491114:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
1862607:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
441437:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
1252325:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
845157:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
1097701:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
111674:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
469922:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c22fcb545cb7b0f7f27c11adc702bd5e
Cycle=Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR
Relax podrr007 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr007 2.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr008
"Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwz 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr008 Allowed
Histogram (72 states)
10 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
7 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
29 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
55 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
854 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
132 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
185 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1598 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1442 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
772 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
885 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8419 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
3420 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
4471 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
530 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
3062 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
12255 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2661 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
9986 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2786 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
4414 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
11940 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
15935 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
56254 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
34798 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
14710 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
65880 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
97928 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
14986 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
48585 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4905 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
490 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
60275 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8374 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
29994 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
25320 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
81564 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
83747 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
113224:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
73447 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
121765:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
74738 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
145872:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
102300:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
97938 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
89446 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
118830:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
103555:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
59065 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
70065 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
75604 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
91892 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
91191 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
60532 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
86063 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
635681:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
116310:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
377135:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1128848:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
85770 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
618585:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1023492:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
392652:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
446638:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
610624:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
558881:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
107005:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1229774:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
393902:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2069502:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2892382:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1023634:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=58c192e74d841e0ccb20b3014a58a473
Cycle=Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR
Relax podrr008 No PodRR
Safe=Fre BCSyncsWW
Time podrr008 2.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr009
"Fre SyncdWW Rfe SyncsRW Rfe PodRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,2 | ;
li r3,1 | stw r3,0(r2) | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 31,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 10,2
_litmus_P1_3_: stw 10,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test podrr009 Allowed
Histogram (14 states)
3 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
1814765:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
1739382:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
563696:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
1522635:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
313552:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
2433649:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
383420:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
1189244:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
504217:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
2387860:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
1061961:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
1651422:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
5434194:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=d6249053a9b844d8e7a3045b38500a3a
Cycle=Fre SyncdWW Rfe SyncsRW Rfe PodRR
Relax podrr009 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW
Time podrr009 1.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr010
"Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,2 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r2) | ;
stw r3,0(r4) | | | ;
exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 10,2
_litmus_P2_3_: stw 10,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test podrr010 Allowed
Histogram (31 states)
49387 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
137509:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
52611 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
72737 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
181016:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
475149:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
97639 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
63324 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
666213:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
136974:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
122552:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
657163:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
69414 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
301470:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
143330:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
580864:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
379381:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
318845:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
66211 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
188155:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
1059024:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
1014290:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
235721:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
266481:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
1450203:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
1836176:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
1414287:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
1094206:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
1158078:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1030821:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
680769:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=fcb68021656d7cbdb455ef5bd2648d65
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR
Relax podrr010 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr010 2.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr011
"Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,2 | ;
li r3,2 | stw r3,0(r4) | stw r3,0(r2) | ;
stw r3,0(r2) | | | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: lwz 31,0(9)
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 10,2
_litmus_P2_3_: stw 10,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test podrr011 Allowed
Histogram (66 states)
504 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
2385 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
3439 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
7760 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
4649 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
39185 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
703 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
10567 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
3684 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
764 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
13515 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
15527 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
23512 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
15196 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
3954 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
8520 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
23085 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
12524 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
7803 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
26561 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
27840 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
80648 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
29407 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
77977 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
14286 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
12574 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
16023 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
39509 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
18682 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
89835 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
45952 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
52318 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
61269 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
67821 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
83736 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
35168 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
142126:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
28112 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
68675 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
87610 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
67078 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
690718:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
42112 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
293003:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
120594:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
977789:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
210053:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
69486 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
495362:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
748147:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
292761:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
225084:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
205993:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
1027087:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
912312:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
1447461:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
564941:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
904926:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
278345:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
522084:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
737280:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
1575654:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
1453751:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
208461:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
287525:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
338588:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=a463a88f960487eded38b9c473eec1b5
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR
Relax podrr011 No PodRR
Safe=Fre BCSyncsWW BCSyncsRW BCSyncdRW
Time podrr011 2.10
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 100000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 10
#endif
#ifndef N_EXE
#define N_EXE (64 < N ? 1 : 64 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread -maix64 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 64 */
GCCOPTS="-Wall -std=gnu99 -O -pthread -maix64"
LITMUSOPTS=
Wed Dec 23 13:46:50 NFT 2009