Wed Dec 23 13:45:17 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)
11576545:>1:r1=1; 1:r3=1;
4714098:>1:r1=0; 1:r3=1;
15709357:>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 1.70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
115761:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
192003:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1305544:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1024923:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
88929 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1815336:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
132800:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1063624:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1393182:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1011065:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
3384431:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1134156:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1595234:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
1571613:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
171399:>1:r1=0; 1:r3=0; 3:r1=1; 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.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1695 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
4925 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
62721 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
83423 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
61803 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
13460 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
254905:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
215214:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
216923:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
87277 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
980022:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
51878 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
107760:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
43958 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
129541:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
809446:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
180671:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
624338:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
158961:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
82168 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
87500 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
185859:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
366464:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1965780:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
181491:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
43481 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1328769:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1071758:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
985971:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
16252 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
3091170:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1177580:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1326836:>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 3.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1086389:>1:r1=1; 2:r1=1; 2:r3=1;
1877416:>1:r1=0; 2:r1=1; 2:r3=0;
4358892:>1:r1=1; 2:r1=0; 2:r3=1;
1776972:>1:r1=1; 2:r1=0; 2:r3=0;
817726:>1:r1=0; 2:r1=0; 2:r3=1;
4961852:>1:r1=0; 2:r1=1; 2:r3=1;
6120753:>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.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
114469:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
76152 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
132911:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
104174:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1414550:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
819727:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
2982847:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
814501:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
1811988:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
1662603:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
1256281:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
1331573:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
1132593:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
2218675:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
126956:>1:r1=1; 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 4.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
362 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
9014 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
35577 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
62358 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
75113 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
18612 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
39531 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
11636 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
52315 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
32862 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
63950 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
185593:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
127609:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
61300 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
127845:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
36218 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
204193:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
48801 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
128715:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
270749:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
179065:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
125229:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
663721:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
147443:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
1561409:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1195270:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
1252477:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
900171:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
941715:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
979577:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1376704:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
2708083:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
2376783:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; 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 6.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)
19683 :>1:r1=1; 2:r1=1; 2:r3=1; y=2;
409642:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
283557:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
180984:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
401787:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
29148 :>1:r1=0; 2:r1=0; 2:r3=1; y=2;
2040975:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
421359:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
144493:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
94229 :>1:r1=1; 2:r1=0; 2:r3=2; y=2;
1800336:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
4636033:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
3250740:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
4457956:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
2829078:>1:r1=2; 2:r1=0; 2:r3=0; 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.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
21871 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
148277:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
132582:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
126918:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
123964:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
433845:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
49812 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
34967 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1128472:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
94132 :>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
159606:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
201722:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
398991:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
83721 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
206040:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
1919082:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
609400:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
962496:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
100634:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
427594:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
87973 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
575168:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
1420882:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
796452:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
1441627:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
298481:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
1023184:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
232135:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
1302799:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
1168013:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
289160:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; 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 6.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (73 states)
111 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
186 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1606 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
281 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
332 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
42 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1181 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
238 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4384 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1004 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1884 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
11169 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
14743 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1261 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2971 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
808 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4475 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
5691 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
21101 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
23229 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
23659 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
39873 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
28227 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5903 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
11136 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
30143 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
19290 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
18570 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
61179 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
79373 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
80018 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
90242 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
96229 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
84670 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
83942 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
155845:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
39290 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
82017 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
95095 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
26282 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
171487:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
70335 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
71862 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
89050 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
146094:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
47217 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
181092:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
146262:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
50406 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
106083:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
159173:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
361092:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
115515:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
128304:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
340213:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
97741 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
96319 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
982363:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
72747 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
107399:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
375392:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
116085:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
570392:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2218438:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
633324:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
985326:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
379375:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
546643:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1067353:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2785678:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
955732:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
577827:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 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 6.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
1789309:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
1157987:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
1817676:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
436390:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
573023:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
1835295:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
497870:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
1099656:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
313741:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
1538716:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
2296104:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
5205143:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
2439087:>1:r1=0; 2:r1=1; 2:r3=1; 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 3.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
32104 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
182441:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
130869:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
101302:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
104456:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
96229 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
95570 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
50298 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
243966:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
48722 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
481465:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
102234:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
39830 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
623238:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
218534:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
133319:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
276567:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
228327:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
623400:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
416093:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
313797:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
1082371:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
380766:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
1174961:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
1021114:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
1449631:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
1511866:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
1792617:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
1165949:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
609948:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
1268016:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; 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 6.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
263 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
7555 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
13379 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
496 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
8026 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
21426 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
7110 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
10132 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
28918 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
80634 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
20015 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
382 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
41789 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
5457 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
6935 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
30325 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
31789 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
25775 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
35347 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
2974 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
61561 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
38944 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
66453 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
192716:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
19071 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
42106 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
93580 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
36127 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
88879 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
171187:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
103794:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
61831 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
26808 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
87689 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
13210 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
70736 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
179883:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
51905 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
10661 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
74457 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
283998:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
50183 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
81381 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
237366:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
49740 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
381282:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
267694:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
183565:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
214388:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
1043382:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
565065:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
662675:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
803967:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
28289 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
277442:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
409125:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
37924 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
1421185:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
844812:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
898533:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
1457681:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
962128:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
283437:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
1460742:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
697101:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
526590:>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 6.26
$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:15 NFT 2009