Wed Dec 23 13:38:15 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)
10849475:>1:r1=1; 1:r3=1;
6293338:>1:r1=0; 1:r3=1;
14857187:>1:r1=0; 1:r3=0;
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 2.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
186947:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
169856:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
124706:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
172408:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
121055:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1106399:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1066688:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
957047:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1394747:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1289923:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1587713:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
898866:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
1744457:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
3379659:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1799529:>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 9.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1422 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
5105 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
19329 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
62924 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
10744 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
137108:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
74099 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
229716:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
112026:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
64012 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
57142 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
30766 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
41593 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
51792 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
67149 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
174064:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
77023 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
235578:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
112514:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
213225:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1204876:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1339455:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
165679:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1890217:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1565764:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
370197:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
939740:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1232410:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
917717:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
746160:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
173212:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
691396:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
2985846:>1:r1=0; 1:r3=0; 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 5.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1163203:>1:r1=1; 2:r1=1; 2:r3=1;
1664397:>1:r1=1; 2:r1=0; 2:r3=0;
4376761:>1:r1=1; 2:r1=0; 2:r3=1;
1844890:>1:r1=0; 2:r1=1; 2:r3=0;
4724231:>1:r1=0; 2:r1=1; 2:r3=1;
977884:>1:r1=0; 2:r1=0; 2:r3=1;
6248634:>1:r1=0; 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 4.71
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
91823 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
67382 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
114318:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
714743:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
130727:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
1066433:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
1518563:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
1429905:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
2129067:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
202910:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1357166:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
2754000:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
795586:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
1940422:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
1686955:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
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 8.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
17239 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
285 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
27695 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
69565 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
20386 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
94844 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
32977 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
50175 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
60603 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
50244 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
68892 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
148485:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
87143 :>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
253248:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
124633:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
144408:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
43537 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
64361 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
57212 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
156171:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
237781:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
188361:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
221577:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
561702:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
859501:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1559750:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1073391:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
2421161:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
2513925:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
1499423:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
1080409:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
861182:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1349734:>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 7.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
43283 :>1:r1=0; 2:r1=0; 2:r3=1; y=2;
399133:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
299354:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
184940:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
22776 :>1:r1=1; 2:r1=1; 2:r3=1; y=2;
345325:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
195835:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
104587:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
2083288:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
468531:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
4775544:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
4367016:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
3118641:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
2669851:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
1921896:>1:r1=2; 2:r1=1; 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 4.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
27037 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
114063:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
18645 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
120054:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
129843:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
287256:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
704583:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
50518 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
1008363:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
352890:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
90190 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
125874:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
209796:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
259263:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
277725:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
1329364:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
103719:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
132415:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
443267:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
1049707:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
398612:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
702804:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
320814:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
554408:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
1279722:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
99935 :>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
1098337:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
1852381:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
111661:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1119214:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
1627540:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
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 14.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (74 states)
4 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
913 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2573 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
93 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
183 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
518 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
237 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
496 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
12528 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1225 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
611 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
428 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2996 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
9258 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
10247 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
784 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
4867 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
12996 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2689 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
24745 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1556 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1802 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
20136 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
23600 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
20622 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
44881 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
43691 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
70781 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5509 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
113890:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
135153:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
126825:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
64735 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
151126:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
104468:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
18415 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
78431 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
39161 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
21884 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
139557:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
151005:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
20621 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
63073 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
106285:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
8718 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
75338 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
105454:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
60210 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
122343:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
65764 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
61272 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
128452:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
375660:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
113253:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
107014:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
111272:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
102211:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
142373:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
72603 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
710376:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
239652:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
666516:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
603672:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
995805:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
986567:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
620726:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1030886:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
329776:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
366725:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2496559:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2124371:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1126760:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
394072:>1:r1=2; 1:r3=0; 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 14.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (13 states)
252009:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
1630387:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
1468364:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
2186986:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
1556118:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
1690366:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
1033474:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
564105:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
672836:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
1309075:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
696213:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
2981886:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
4958181:>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 11.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
89225 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
97161 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
200419:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
129720:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
51575 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
32347 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
45288 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
39725 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
253655:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
207470:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
549801:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
122419:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
117840:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
936522:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
315178:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
444101:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
121095:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
1093289:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
354109:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
596501:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
244552:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
1254180:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
596990:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
140887:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
1668949:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
576664:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
282556:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
1355284:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
1801275:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
1194014:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
1087209:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
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 18.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
358 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
630 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
1094 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
6937 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
33572 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
8567 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
4542 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
23536 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
7850 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
82959 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
28012 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
9431 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
13533 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
42345 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
12246 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
25816 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
27749 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
239350:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
10197 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
72867 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
62208 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
87336 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
54596 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
27917 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
32334 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
53043 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
22178 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
409696:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
17937 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
58026 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
10595 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
44710 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
74373 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
55284 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
364620:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
183472:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
89984 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
110612:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
31453 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
9936 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
226120:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
39354 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
561181:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
814779:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
72548 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
47826 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
87958 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
256338:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
1401822:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
222725:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
247104:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
314100:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
48615 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
48624 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
806898:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
222921:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
166100:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
810109:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
693217:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
1323838:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
676505:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
1678834:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
238271:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
1040118:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
1009985:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
492209:>1:r1=0; 2:r1=0; 3:r1=2; 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 18.96
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 100000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 10
#endif
#ifndef N_EXE
#define N_EXE (64 < N ? 1 : 64 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread -maix64 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 64 */
GCCOPTS="-Wall -std=gnu99 -O -pthread -maix64"
LITMUSOPTS=
Wed Dec 23 13:40:19 NFT 2009