Wed Dec 23 13:42:32 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)
10632473:>1:r1=1; 1:r3=1;
14565878:>1:r1=0; 1:r3=0;
6801649:>1:r1=0; 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 2.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
107316:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
112704:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
112356:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
178147:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1085303:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
172968:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
952551:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1109031:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1640085:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
973728:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
1368605:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
3507397:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1227334:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1769917:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
1682558:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
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 6.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
889 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
37533 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
221692:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
79174 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
13862 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
3874 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
195168:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
51172 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
39510 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
46601 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
98035 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
249458:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
48076 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
203461:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
864115:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
45819 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
151257:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
157368:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
68937 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
48677 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
175153:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
746823:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
197014:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1101841:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
987906:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
16677 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1995704:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
2949936:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
381099:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1183017:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1290981:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
855913:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1493258:>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 7.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1251163:>1:r1=1; 2:r1=1; 2:r3=1;
1858941:>1:r1=0; 2:r1=1; 2:r3=0;
4479884:>1:r1=1; 2:r1=0; 2:r3=1;
714529:>1:r1=0; 2:r1=0; 2:r3=1;
6008058:>1:r1=0; 2:r1=0; 2:r3=0;
4796325:>1:r1=0; 2:r1=1; 2:r3=1;
1891100:>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 3.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
110957:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
120654:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
72674 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
857915:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
132521:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
726439:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
1550522:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
1095844:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
1250074:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
181126:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1535377:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
2980731:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
2056623:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
2040927:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
1287616:>1:r1=1; 2:r1=0; 3:r1=0; 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 6.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
772 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
39087 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
49105 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
35354 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
9434 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
48461 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
7879 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
8013 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
54751 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
47881 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
132309:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
48388 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
12760 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
188406:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
86404 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
120853:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
112027:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
76835 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
1252813:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
110613:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
1258945:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
167762:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
854916:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
1468625:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
258795:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
107410:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
2478902:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
685737:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
37666 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
1580337:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
928142:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
2767650:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
962968:>1:r1=2; 2:r1=1; 3:r1=0; 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 2.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
293041:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
383019:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
227528:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
2216611:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
414375:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
25164 :>1:r1=0; 2:r1=0; 2:r3=1; y=2;
25336 :>1:r1=1; 2:r1=1; 2:r3=1; y=2;
223790:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
76067 :>1:r1=1; 2:r1=0; 2:r3=2; y=2;
4358973:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
121397:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
3111003:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
1871904:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
4877477:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
2774315:>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 2.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)
64732 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
106515:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
115659:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
108403:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
20326 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
84614 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
20183 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
283094:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
135868:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
452870:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
80436 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
233480:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
132270:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
100324:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
440562:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
216153:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
705072:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
116281:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
1117637:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
904079:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
422271:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
841248:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
1924437:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
1237163:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
1624949:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
225770:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
1229733:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
1084344:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
301359:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
468005:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
1202163:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; 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 4.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
29 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
112 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
827 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
55 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1050 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
201 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3624 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
773 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2279 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
9319 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
737 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
199 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
14897 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
836 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
8897 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2554 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4889 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
19005 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
16559 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
113491:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3295 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
29847 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
187 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
11853 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
70153 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
19454 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
138643:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
83387 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
76544 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
67154 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
66673 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
10108 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
31135 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
61298 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
135255:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
74079 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
79145 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
109855:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
133155:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
18844 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
98226 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
626873:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
144902:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
17353 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
695 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
66148 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
51358 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
63288 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
65516 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
15107 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
117001:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
129197:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
38220 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
344555:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
57519 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1064897:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
79531 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2941341:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
591076:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
76945 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
73358 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
151527:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
84788 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2291955:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
610785:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
362326:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
628468:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
347128:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
971025:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
994360:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
335268:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1138867:>1:r1=2; 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.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
297404:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
623375:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
1773453:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
545264:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
569266:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
2653521:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
2177272:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
1632670:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
1225733:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
1428829:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
1099189:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
5270011:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
1704007:>1:r1=0; 2:r1=2; 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 4.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
47596 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
94915 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
202574:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
99177 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
38741 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
118210:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
163991:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
61952 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
105895:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
491074:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
258573:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
53275 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
56417 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
742166:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
1438456:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
440677:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
60852 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
680229:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
275554:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
1127068:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
215055:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
1066988:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
1618736:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
1034135:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
153316:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
385867:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
323467:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
599105:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
1816950:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
1109733:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
1119256:>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.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
678 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
465 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
776 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
4125 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
7981 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
4967 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
5703 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
54856 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
20928 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
38794 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
11536 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
10323 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
15890 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
16779 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
16480 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
5887 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
5453 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
38185 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
59982 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
56692 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
53512 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
234817:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
67602 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
36861 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
35836 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
20612 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
86980 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
55095 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
70250 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
18971 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
12104 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
31746 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
47157 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
93612 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
189311:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
508999:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
24341 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
703619:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
59908 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
41792 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
206710:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
155600:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
10128 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
89869 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
883110:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
404897:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
81159 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
280083:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
333680:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
255542:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
1343091:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
117932:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
22399 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
249879:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
880685:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
80206 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
685701:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
744038:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
1704365:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
272738:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
1475786:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
944587:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
984550:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
413599:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
572167:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
37894 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; 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.37
$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:43:33 NFT 2009