Wed Dec 23 18:57:21 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfe000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfe000
"DpdW Rfe DpdW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 ;
li r4,1 | li r4,1 ;
stwx r4,r3,r5 | stwx r4,r3,r5 ;
exists (0:r1=1 /\ 1:r1=1)
Generated assembler
_litmus_P0_0_: lwz r7,0(r9)
_litmus_P0_1_: xor r11,r7,r7
_litmus_P0_2_: li r8,1
_litmus_P0_3_: stwx r8,r11,r2
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
Test rfe000 Allowed
Histogram (3 states)
213003:>0:r1=0; 1:r1=0;
966314:>0:r1=0; 1:r1=1;
820683:>0:r1=1; 1:r1=0;
No
Witnesses
Positive: 0, Negative: 2000000
Condition exists (0:r1=1 /\ 1:r1=1) is NOT validated
Hash=467bf017bb8c30b6aa0f5da2e165fe50
Cycle=DpdW Rfe DpdW Rfe
Relax rfe000 No Rfe
Safe=DpdW
Time rfe000 1.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfe001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfe001
"DpdW Rfe DpdW Rfe DpdW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 | xor r3,r1,r1 ;
li r4,1 | li r4,1 | li r4,1 ;
stwx r4,r3,r5 | stwx r4,r3,r5 | stwx r4,r3,r5 ;
exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1)
Generated assembler
_litmus_P0_0_: lwz r7,0(r9)
_litmus_P0_1_: xor r11,r7,r7
_litmus_P0_2_: li r8,1
_litmus_P0_3_: stwx r8,r11,r2
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: xor r11,r7,r7
_litmus_P2_2_: li r8,1
_litmus_P2_3_: stwx r8,r11,r2
Test rfe001 Allowed
Histogram (7 states)
5371 :>0:r1=1; 1:r1=1; 2:r1=0;
10084 :>0:r1=1; 1:r1=0; 2:r1=1;
268075:>0:r1=1; 1:r1=0; 2:r1=0;
304395:>0:r1=0; 1:r1=1; 2:r1=0;
273662:>0:r1=0; 1:r1=0; 2:r1=1;
5117 :>0:r1=0; 1:r1=1; 2:r1=1;
133296:>0:r1=0; 1:r1=0; 2:r1=0;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) is NOT validated
Hash=bced5ef4373b299015cfac677ee91a60
Cycle=DpdW Rfe DpdW Rfe DpdW Rfe
Relax rfe001 No Rfe
Safe=DpdW
Time rfe001 1.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfe002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfe002
"DpdW Wse Rfe DpdW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=x; 2:r2=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | li r1,2 ;
xor r3,r1,r1 | xor r3,r1,r1 | stw r1,0(r2) ;
li r4,1 | li r4,1 | ;
stwx r4,r3,r5 | stwx r4,r3,r5 | ;
exists (x=2 /\ 0:r1=2 /\ 1:r1=1)
Generated assembler
_litmus_P0_0_: lwz r7,0(r9)
_litmus_P0_1_: xor r11,r7,r7
_litmus_P0_2_: li r8,1
_litmus_P0_3_: stwx r8,r11,r2
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: xor r11,r7,r7
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stwx r8,r11,r2
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
Test rfe002 Allowed
Histogram (9 states)
1239 :>0:r1=0; 1:r1=1; x=2;
153017:>0:r1=1; 1:r1=0; x=2;
21566 :>0:r1=2; 1:r1=1; x=1;
31611 :>0:r1=0; 1:r1=0; x=1;
97417 :>0:r1=1; 1:r1=0; x=1;
10399 :>0:r1=0; 1:r1=0; x=2;
136838:>0:r1=2; 1:r1=0; x=2;
303849:>0:r1=0; 1:r1=1; x=1;
244064:>0:r1=2; 1:r1=0; x=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ 0:r1=2 /\ 1:r1=1) is NOT validated
Hash=381e1f1a657547032657db7160e7a70d
Cycle=DpdW Wse Rfe DpdW Rfe
Relax rfe002 No Rfe
Safe=Wse DpdW
Time rfe002 1.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfe003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfe003
"DpdR Fre Rfe DpdW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=x; 2:r2=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | li r1,1 ;
xor r3,r1,r1 | xor r3,r1,r1 | stw r1,0(r2) ;
li r4,1 | lwzx r4,r3,r5 | ;
stwx r4,r3,r5 | | ;
exists (0:r1=1 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P0_0_: lwz r7,0(r9)
_litmus_P0_1_: xor r11,r7,r7
_litmus_P0_2_: li r8,1
_litmus_P0_3_: stwx r8,r11,r2
_litmus_P1_0_: lwz r6,0(r9)
_litmus_P1_1_: xor r11,r6,r6
_litmus_P1_2_: lwzx r7,r11,r2
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
Test rfe003 Allowed
Histogram (7 states)
6848 :>0:r1=0; 1:r1=1; 1:r4=0;
23515 :>0:r1=0; 1:r1=0; 1:r4=1;
144698:>0:r1=1; 1:r1=0; 1:r4=0;
335037:>0:r1=1; 1:r1=0; 1:r4=1;
168812:>0:r1=0; 1:r1=0; 1:r4=0;
306030:>0:r1=0; 1:r1=1; 1:r4=1;
15060 :>0:r1=1; 1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (0:r1=1 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=36c82af8fb9a7ec1207fcf0cad98aabe
Cycle=DpdR Fre Rfe DpdW Rfe
Relax rfe003 No Rfe
Safe=Fre DpdW DpdR
Time rfe003 1.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfe004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfe004
"DpdW Wse Rfe DpdW Wse Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r5=x; 3:r2=x;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,2 ;
xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ;
li r4,1 | | li r4,1 | ;
stwx r4,r3,r5 | | stwx r4,r3,r5 | ;
exists (x=2 /\ y=2 /\ 0:r1=2 /\ 2:r1=2)
Generated assembler
_litmus_P0_0_: lwz r7,0(r9)
_litmus_P0_1_: xor r11,r7,r7
_litmus_P0_2_: li r8,1
_litmus_P0_3_: stwx r8,r11,r2
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: xor r11,r7,r7
_litmus_P2_2_: li r8,1
_litmus_P2_3_: stwx r8,r11,r2
_litmus_P3_0_: li r9,2
_litmus_P3_1_: stw r9,0(r2)
Test rfe004 Allowed
Histogram (27 states)
94 :>0:r1=0; 2:r1=1; x=2; y=1;
526 :>0:r1=2; 2:r1=0; x=2; y=2;
2529 :>0:r1=0; 2:r1=2; x=2; y=2;
4386 :>0:r1=2; 2:r1=1; x=1; y=2;
4869 :>0:r1=2; 2:r1=2; x=1; y=2;
6189 :>0:r1=1; 2:r1=2; x=2; y=1;
11042 :>0:r1=1; 2:r1=0; x=2; y=2;
8373 :>0:r1=2; 2:r1=2; x=2; y=1;
2097 :>0:r1=0; 2:r1=0; x=1; y=2;
911 :>0:r1=0; 2:r1=0; x=2; y=2;
5510 :>0:r1=0; 2:r1=1; x=2; y=2;
15024 :>0:r1=2; 2:r1=0; x=1; y=2;
18673 :>0:r1=0; 2:r1=1; x=1; y=1;
14295 :>0:r1=1; 2:r1=0; x=1; y=1;
1462 :>0:r1=0; 2:r1=0; x=2; y=1;
1147 :>0:r1=0; 2:r1=0; x=1; y=1;
57619 :>0:r1=0; 2:r1=2; x=1; y=1;
49052 :>0:r1=2; 2:r1=1; x=1; y=1;
182701:>0:r1=2; 2:r1=2; x=1; y=1;
112986:>0:r1=1; 2:r1=0; x=2; y=1;
75276 :>0:r1=1; 2:r1=2; x=1; y=1;
73294 :>0:r1=0; 2:r1=1; x=1; y=2;
35427 :>0:r1=2; 2:r1=0; x=1; y=1;
37229 :>0:r1=0; 2:r1=2; x=2; y=1;
121554:>0:r1=2; 2:r1=0; x=2; y=1;
157642:>0:r1=0; 2:r1=2; x=1; y=2;
93 :>0:r1=1; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 0:r1=2 /\ 2:r1=2) is NOT validated
Hash=3ff9f33d19c19af532626ad01e67e950
Cycle=DpdW Wse Rfe DpdW Wse Rfe
Relax rfe004 No Rfe
Safe=Wse DpdW
Time rfe004 1.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfe005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfe005
"DpdR Fre Rfe DpdW Wse Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r5=x; 3:r2=x;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ;
xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ;
li r4,1 | | lwzx r4,r3,r5 | ;
stwx r4,r3,r5 | | | ;
exists (y=2 /\ 0:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P0_0_: lwz r7,0(r9)
_litmus_P0_1_: xor r11,r7,r7
_litmus_P0_2_: li r8,1
_litmus_P0_3_: stwx r8,r11,r2
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r6,0(r9)
_litmus_P2_1_: xor r11,r6,r6
_litmus_P2_2_: lwzx r7,r11,r2
_litmus_P3_0_: li r9,1
_litmus_P3_1_: stw r9,0(r2)
Test rfe005 Allowed
Histogram (21 states)
135 :>0:r1=1; 2:r1=0; 2:r4=0; y=2;
2778 :>0:r1=1; 2:r1=1; 2:r4=1; y=2;
1183 :>0:r1=0; 2:r1=1; 2:r4=0; y=2;
1897 :>0:r1=0; 2:r1=2; 2:r4=0; y=2;
1001 :>0:r1=0; 2:r1=1; 2:r4=0; y=1;
12111 :>0:r1=1; 2:r1=0; 2:r4=1; y=2;
22255 :>0:r1=0; 2:r1=1; 2:r4=1; y=1;
1108 :>0:r1=0; 2:r1=0; 2:r4=1; y=1;
58222 :>0:r1=1; 2:r1=1; 2:r4=1; y=1;
16705 :>0:r1=0; 2:r1=0; 2:r4=0; y=2;
674 :>0:r1=0; 2:r1=0; 2:r4=1; y=2;
36791 :>0:r1=1; 2:r1=0; 2:r4=1; y=1;
47067 :>0:r1=0; 2:r1=2; 2:r4=1; y=1;
12781 :>0:r1=1; 2:r1=2; 2:r4=0; y=1;
38407 :>0:r1=0; 2:r1=2; 2:r4=0; y=1;
169658:>0:r1=0; 2:r1=0; 2:r4=0; y=1;
71853 :>0:r1=0; 2:r1=1; 2:r4=1; y=2;
270509:>0:r1=1; 2:r1=2; 2:r4=1; y=1;
60702 :>0:r1=1; 2:r1=0; 2:r4=0; y=1;
168521:>0:r1=0; 2:r1=2; 2:r4=1; y=2;
5642 :>0:r1=1; 2:r1=2; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ 0:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=38f61d39ea6d477ceb57de4910657abe
Cycle=DpdR Fre Rfe DpdW Wse Rfe
Relax rfe005 No Rfe
Safe=Fre Wse DpdW DpdR
Time rfe005 1.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfe006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfe006
"DpdR Fre Rfe DpdR Fre Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r5=x; 3:r2=x;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ;
lwzx r4,r3,r5 | | lwzx r4,r3,r5 | ;
exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0)
Generated assembler
_litmus_P0_0_: lwz r6,0(r9)
_litmus_P0_1_: xor r11,r6,r6
_litmus_P0_2_: lwzx r7,r11,r2
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r6,0(r9)
_litmus_P2_1_: xor r11,r6,r6
_litmus_P2_2_: lwzx r7,r11,r2
_litmus_P3_0_: li r9,1
_litmus_P3_1_: stw r9,0(r2)
Test rfe006 Allowed
Histogram (15 states)
1857 :>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0;
1082 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1;
6052 :>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0;
1015 :>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1;
20586 :>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0;
29618 :>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0;
38100 :>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1;
18251 :>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1;
67467 :>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0;
175706:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0;
19032 :>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0;
368747:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1;
56064 :>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1;
190234:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1;
6189 :>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=8352ce27483f00d649cb0bf6b7f9ba8b
Cycle=DpdR Fre Rfe DpdR Fre Rfe
Relax rfe006 No Rfe
Safe=Fre DpdR
Time rfe006 1.55
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=
Wed Dec 23 18:57:31 CET 2009