Mon Dec 28 11:05:12 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)
114206384:>1:r1=1; 1:r3=1;
48221865:>1:r1=0; 1:r3=1;
157571751:>1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
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 14.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1185499:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1208483:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
910112:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
2007862:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1981318:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
9834283:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
12832189:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
11505919:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
17332410:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
15923436:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
15901836:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
11398406:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
10056879:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
12882962:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
35038406:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 160000000
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 22.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
39838 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
18615 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
440153:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1168489:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
109716:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1658287:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
404707:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
724427:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
2179577:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
839978:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1365386:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
811609:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
519351:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1279998:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
2287135:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
494941:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
2035044:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
152012:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
3681347:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
6665964:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
2213759:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
505244:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
9221345:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
13646101:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
797929:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1105883:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
7782465:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
10217836:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
12062012:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
31749059:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
19615764:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
12903533:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
11302496:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 22.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
12353240:>1:r1=1; 2:r1=1; 2:r3=1;
5613525:>1:r1=0; 2:r1=0; 2:r3=1;
19079074:>1:r1=1; 2:r1=0; 2:r3=0;
44069561:>1:r1=1; 2:r1=0; 2:r3=1;
47313741:>1:r1=0; 2:r1=1; 2:r3=1;
60712615:>1:r1=0; 2:r1=0; 2:r3=0;
20858244:>1:r1=0; 2:r1=1; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 210000000
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 18.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1409768:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
1089148:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
661170:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
1352363:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
7956133:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
11049158:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
1324925:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
7717100:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
13380372:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
16075881:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
29935769:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
13856210:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
13305014:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
19117267:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
21769722:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 160000000
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 22.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)
6205 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
128491:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
82997 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
1516378:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
357252:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
552721:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
1276483:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
701695:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
474252:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
1197841:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
587317:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
6771630:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
231009:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
194967:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
525031:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
8175776:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
497034:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
1197313:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
1278956:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
2694794:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
416563:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
788879:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
12290592:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
12368544:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
9764112:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
9134292:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
15534661:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
27765355:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
2065185:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1347659:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
24308681:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
13611472:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
2155863:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 22.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
256726:>1:r1=1; 2:r1=1; 2:r3=1; y=2;
275162:>1:r1=0; 2:r1=0; 2:r3=1; y=2;
2567917:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
2158542:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
835150:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
3006794:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
4361183:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
3867592:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
21975720:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
19126590:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
1193833:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
27996764:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
43018536:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
47676871:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
31682620:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 210000000
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 17.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
240561:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1117610:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
1298318:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1185995:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
1546997:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
283442:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
4253171:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
1318617:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
717134:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
10527823:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
5102142:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
2818639:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
2150157:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
12861629:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
1911769:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
4998230:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
672409:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
6777150:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
4593464:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
2474987:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
11964445:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
8791536:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
705441:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
10557473:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
9065803:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
1145192:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
1181064:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
12620349:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
3079574:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
18993522:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
15045357:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 160000000
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 22.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
253 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1935 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1759 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
230 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
5619 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
15133 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
543 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
104 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
8555 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
7994 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
35799 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
12436 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
41254 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
54482 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
47451 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
32406 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
600651:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
118674:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
36408 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
137545:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
141153:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
173270:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
35807 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
965988:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
9696 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
94541 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
5695 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
217683:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
117845:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
127624:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
661212:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
96817 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1054264:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
674925:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
573952:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
693650:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
755014:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
203551:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
752541:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1049854:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
678894:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
663012:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
833555:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1137197:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1015034:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
626059:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
669186:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
731445:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1185005:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1423790:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
805414:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1175891:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1147476:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4059531:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
852624:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
706507:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1152863:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1180412:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
6329662:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
10364746:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
6164601:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3563809:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
6004072:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1372406:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3598852:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
6385407:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4022998:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
11181866:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
11316833:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
28160314:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
10418811:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
21507415:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 22.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
37 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
18177557:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
3184114:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
4789484:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
6048421:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
11826198:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
14694212:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
23354080:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
3841729:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
24695410:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
10848213:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
18391810:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
52967050:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
17181685:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 210000000
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 17.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
598536:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
1019911:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
1271282:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
1247240:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
3288166:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
694382:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
6830755:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
567291:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
484858:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
6146561:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
1322799:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
5082181:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
1317637:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
1547078:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
1835888:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
2536813:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
10884001:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
14651843:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
2519004:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
14936506:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
10512614:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
3517755:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
18092929:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
11511878:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
10963886:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
10107845:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
606825:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
3113345:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
5406043:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
552554:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
6831594:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 160000000
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 22.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5711 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
8080 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
48952 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
198108:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
57886 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
165385:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
224557:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
125430:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
11063 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
250727:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
82269 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
366216:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
928477:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
246355:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
57358 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
135080:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
55146 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
105817:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
322174:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
33556 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
87802 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
153800:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
503182:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
163812:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
395310:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
624256:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
233771:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
645991:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
2097627:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
2828974:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
738702:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
345163:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
2872422:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
646405:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
4429825:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
1049121:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
420633:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
364177:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
2336490:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
445065:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
3017821:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
787315:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
532408:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
2109002:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
2780370:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
864355:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
960764:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
5342710:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
2314123:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
695873:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
1672363:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
3564188:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
893011:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
453242:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
136047:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
9494363:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
6991448:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
8296357:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
14068453:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
9128486:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
5647059:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
10260564:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
6980176:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
16009858:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
7005489:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
15183280:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 21.86
$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=-r 100
Mon Dec 28 11:09:22 NFT 2009