Sun Dec 27 15:19:46 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r27,0(r9)
_litmus_P0_1_: xor r30,r27,r27
_litmus_P0_2_: li r11,1
_litmus_P0_3_: stwx r11,r30,r2
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: xor r30,r27,r27
_litmus_P1_2_: li r11,1
_litmus_P1_3_: stwx r11,r30,r2
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
Test rfe002 Allowed
Histogram (9 states)
297797:>0:r1=0; 1:r1=1; x=2;
5794399:>0:r1=1; 1:r1=0; x=2;
1118157:>0:r1=0; 1:r1=0; x=1;
5595771:>0:r1=2; 1:r1=0; x=2;
793931:>0:r1=0; 1:r1=0; x=2;
9644313:>0:r1=2; 1:r1=0; x=1;
2238985:>0:r1=1; 1:r1=0; x=1;
11919531:>0:r1=0; 1:r1=1; x=1;
2597116:>0:r1=2; 1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 34.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r27,0(r9)
_litmus_P0_1_: xor r30,r27,r27
_litmus_P0_2_: li r11,1
_litmus_P0_3_: stwx r11,r30,r2
_litmus_P1_0_: lwz r26,0(r9)
_litmus_P1_1_: xor r11,r26,r26
_litmus_P1_2_: lwzx r27,r11,r2
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
Test rfe003 Allowed
Histogram (7 states)
902274:>0:r1=0; 1:r1=1; 1:r4=0;
1089929:>0:r1=0; 1:r1=0; 1:r4=1;
6264419:>0:r1=1; 1:r1=0; 1:r4=0;
10872892:>0:r1=1; 1:r1=0; 1:r4=1;
7372107:>0:r1=0; 1:r1=0; 1:r4=0;
10925108:>0:r1=0; 1:r1=1; 1:r4=1;
2573271:>0:r1=1; 1:r1=1; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 30.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r27,0(r9)
_litmus_P0_1_: xor r30,r27,r27
_litmus_P0_2_: li r11,1
_litmus_P0_3_: stwx r11,r30,r2
_litmus_P1_0_: li r6,2
_litmus_P1_1_: stw r6,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: xor r30,r27,r27
_litmus_P2_2_: li r11,1
_litmus_P2_3_: stwx r11,r30,r2
_litmus_P3_0_: li r5,2
_litmus_P3_1_: stw r5,0(r2)
Test rfe004 Allowed
Histogram (27 states)
19503 :>0:r1=1; 2:r1=0; x=1; y=2;
13476 :>0:r1=0; 2:r1=1; x=2; y=1;
465815:>0:r1=0; 2:r1=1; x=2; y=2;
178256:>0:r1=0; 2:r1=2; x=2; y=2;
494837:>0:r1=2; 2:r1=0; x=2; y=2;
77450 :>0:r1=0; 2:r1=0; x=2; y=1;
247976:>0:r1=2; 2:r1=1; x=1; y=2;
167491:>0:r1=0; 2:r1=0; x=2; y=2;
43169 :>0:r1=0; 2:r1=0; x=1; y=1;
1242084:>0:r1=1; 2:r1=0; x=2; y=2;
98333 :>0:r1=2; 2:r1=2; x=2; y=1;
1089980:>0:r1=1; 2:r1=0; x=1; y=1;
329946:>0:r1=2; 2:r1=2; x=1; y=2;
637639:>0:r1=2; 2:r1=0; x=1; y=2;
560891:>0:r1=0; 2:r1=2; x=2; y=1;
3404906:>0:r1=0; 2:r1=1; x=1; y=2;
1549117:>0:r1=0; 2:r1=1; x=1; y=1;
76378 :>0:r1=1; 2:r1=2; x=2; y=1;
4319948:>0:r1=2; 2:r1=0; x=2; y=1;
84429 :>0:r1=0; 2:r1=0; x=1; y=2;
7812185:>0:r1=2; 2:r1=2; x=1; y=1;
2326230:>0:r1=1; 2:r1=2; x=1; y=1;
3287003:>0:r1=2; 2:r1=1; x=1; y=1;
1344151:>0:r1=0; 2:r1=2; x=1; y=1;
3506480:>0:r1=1; 2:r1=0; x=2; y=1;
5419320:>0:r1=0; 2:r1=2; x=1; y=2;
1203007:>0:r1=2; 2:r1=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 51.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r27,0(r9)
_litmus_P0_1_: xor r30,r27,r27
_litmus_P0_2_: li r11,1
_litmus_P0_3_: stwx r11,r30,r2
_litmus_P1_0_: li r6,2
_litmus_P1_1_: stw r6,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: xor r11,r27,r27
_litmus_P2_2_: lwzx r30,r11,r2
_litmus_P3_0_: li r5,1
_litmus_P3_1_: stw r5,0(r2)
Test rfe005 Allowed
Histogram (21 states)
541785:>0:r1=0; 2:r1=2; 2:r4=0; y=2;
98719 :>0:r1=1; 2:r1=1; 2:r4=1; y=2;
393188:>0:r1=1; 2:r1=0; 2:r4=0; y=2;
210138:>0:r1=1; 2:r1=2; 2:r4=1; y=2;
57315 :>0:r1=0; 2:r1=1; 2:r4=0; y=1;
926564:>0:r1=0; 2:r1=1; 2:r4=0; y=2;
270259:>0:r1=1; 2:r1=2; 2:r4=0; y=1;
621961:>0:r1=1; 2:r1=0; 2:r4=1; y=2;
72278 :>0:r1=0; 2:r1=0; 2:r4=1; y=1;
190792:>0:r1=0; 2:r1=0; 2:r4=1; y=2;
1531992:>0:r1=0; 2:r1=2; 2:r4=1; y=1;
1787535:>0:r1=0; 2:r1=1; 2:r4=1; y=1;
4482165:>0:r1=1; 2:r1=0; 2:r4=0; y=1;
2482221:>0:r1=0; 2:r1=1; 2:r4=1; y=2;
2856345:>0:r1=1; 2:r1=0; 2:r4=1; y=1;
992537:>0:r1=0; 2:r1=2; 2:r4=0; y=1;
1310827:>0:r1=0; 2:r1=0; 2:r4=0; y=2;
9578177:>0:r1=1; 2:r1=2; 2:r4=1; y=1;
4102737:>0:r1=0; 2:r1=0; 2:r4=0; y=1;
4964429:>0:r1=0; 2:r1=2; 2:r4=1; y=2;
2528036:>0:r1=1; 2:r1=1; 2:r4=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 43.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r27,0(r9)
_litmus_P0_1_: xor r11,r27,r27
_litmus_P0_2_: lwzx r30,r11,r2
_litmus_P1_0_: li r6,1
_litmus_P1_1_: stw r6,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: xor r11,r27,r27
_litmus_P2_2_: lwzx r30,r11,r2
_litmus_P3_0_: li r5,1
_litmus_P3_1_: stw r5,0(r2)
Test rfe006 Allowed
Histogram (15 states)
455532:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0;
261532:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1;
188667:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0;
394195:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0;
4654351:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1;
38900 :>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1;
585606:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0;
4155775:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0;
2197241:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1;
2850124:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1;
3731870:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0;
3254807:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1;
13472125:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1;
3082759:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0;
676516:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1;
No
Witnesses
Positive: 0, Negative: 40000000
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 39.53
$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 -O */
/* 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 -O"
LITMUSOPTS=-r 40 -v
Sun Dec 27 15:23:05 CET 2009