Fri Dec 18 16:22:06 GMT 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_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 4,3,3
_litmus_P0_2_: li 10,1
_litmus_P0_3_: stwx 10,4,9
Test rfe000 Allowed
Histogram (3 states)
3546063:>0:r1=0; 1:r1=0;
318094167:>0:r1=1; 1:r1=0;
318359770:>0:r1=0; 1:r1=1;
No
Witnesses
Positive: 0, Negative: 640000000
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 83.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 31,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,31,9
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 31,30,30
_litmus_P0_2_: li 10,1
_litmus_P0_3_: stwx 10,31,9
Test rfe001 Allowed
Histogram (7 states)
1430320:>0:r1=0; 1:r1=0; 2:r1=0;
33461201:>0:r1=1; 1:r1=0; 2:r1=1;
24460564:>0:r1=1; 1:r1=1; 2:r1=0;
99470575:>0:r1=0; 1:r1=1; 2:r1=0;
106935431:>0:r1=1; 1:r1=0; 2:r1=0;
34607450:>0:r1=0; 1:r1=1; 2:r1=1;
99634459:>0:r1=0; 1:r1=0; 2:r1=1;
No
Witnesses
Positive: 0, Negative: 400000000
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 72.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 31,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,31,9
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 31,3,3
_litmus_P0_2_: li 10,1
_litmus_P0_3_: stwx 10,31,9
Test rfe002 Allowed
Histogram (10 states)
21 :>0:r1=2; 1:r1=1; x=2;
688887:>0:r1=0; 1:r1=0; x=1;
4485827:>0:r1=0; 1:r1=0; x=2;
34226995:>0:r1=2; 1:r1=1; x=1;
64688891:>0:r1=1; 1:r1=0; x=2;
59075747:>0:r1=1; 1:r1=0; x=1;
85086102:>0:r1=0; 1:r1=1; x=1;
43380647:>0:r1=0; 1:r1=1; x=2;
65165157:>0:r1=2; 1:r1=0; x=2;
43201726:>0:r1=2; 1:r1=0; x=1;
Ok
Witnesses
Positive: 21, Negative: 399999979
Condition exists (x=2 /\ 0:r1=2 /\ 1:r1=1) is validated
Hash=381e1f1a657547032657db7160e7a70d
Cycle=DpdW Wse Rfe DpdW Rfe
Relax rfe002 Ok Rfe
Safe=Wse DpdW
Time rfe002 70.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 31,3,3
_litmus_P0_2_: li 10,1
_litmus_P0_3_: stwx 10,31,9
Test rfe003 Allowed
Histogram (8 states)
177 :>0:r1=1; 1:r1=1; 1:r4=0;
28558558:>0:r1=1; 1:r1=1; 1:r4=1;
700995:>0:r1=0; 1:r1=0; 1:r4=1;
76037441:>0:r1=0; 1:r1=1; 1:r4=1;
60150676:>0:r1=1; 1:r1=0; 1:r4=0;
107179817:>0:r1=1; 1:r1=0; 1:r4=1;
51355605:>0:r1=0; 1:r1=1; 1:r4=0;
76016731:>0:r1=0; 1:r1=0; 1:r4=0;
Ok
Witnesses
Positive: 177, Negative: 399999823
Condition exists (0:r1=1 /\ 1:r1=1 /\ 1:r4=0) is validated
Hash=36c82af8fb9a7ec1207fcf0cad98aabe
Cycle=DpdR Fre Rfe DpdW Rfe
Relax rfe003 Ok Rfe
Safe=Fre DpdW DpdR
Time rfe003 72.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_P3_0_: li 7,2
_litmus_P3_1_: stw 7,0(9)
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 4,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,4,9
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 4,3,3
_litmus_P0_2_: li 10,1
_litmus_P0_3_: stwx 10,4,9
Test rfe004 Allowed
Histogram (32 states)
10 :>0:r1=2; 2:r1=1; x=2; y=2;
8 :>0:r1=2; 2:r1=2; x=2; y=2;
7 :>0:r1=1; 2:r1=2; x=2; y=2;
9 :>0:r1=1; 2:r1=2; x=1; y=2;
17 :>0:r1=2; 2:r1=1; x=2; y=1;
136706:>0:r1=0; 2:r1=0; x=1; y=1;
346962:>0:r1=0; 2:r1=0; x=1; y=2;
426794:>0:r1=0; 2:r1=0; x=2; y=1;
1481204:>0:r1=0; 2:r1=0; x=2; y=2;
5174434:>0:r1=2; 2:r1=1; x=1; y=2;
8886367:>0:r1=2; 2:r1=0; x=1; y=2;
6975779:>0:r1=2; 2:r1=0; x=2; y=2;
5602662:>0:r1=1; 2:r1=0; x=1; y=2;
3570942:>0:r1=0; 2:r1=2; x=1; y=1;
19555802:>0:r1=0; 2:r1=1; x=1; y=2;
18893243:>0:r1=1; 2:r1=2; x=1; y=1;
5606837:>0:r1=1; 2:r1=2; x=2; y=1;
3780817:>0:r1=2; 2:r1=0; x=1; y=1;
6693890:>0:r1=2; 2:r1=2; x=1; y=2;
4956702:>0:r1=0; 2:r1=1; x=2; y=1;
17956337:>0:r1=1; 2:r1=0; x=2; y=2;
20850677:>0:r1=1; 2:r1=0; x=1; y=1;
33280921:>0:r1=0; 2:r1=2; x=1; y=2;
7300539:>0:r1=2; 2:r1=2; x=2; y=1;
33568427:>0:r1=2; 2:r1=0; x=2; y=1;
23625359:>0:r1=2; 2:r1=2; x=1; y=1;
18645604:>0:r1=0; 2:r1=1; x=2; y=2;
19534935:>0:r1=0; 2:r1=1; x=1; y=1;
19171971:>0:r1=1; 2:r1=0; x=2; y=1;
18672585:>0:r1=2; 2:r1=1; x=1; y=1;
6512994:>0:r1=0; 2:r1=2; x=2; y=2;
8790459:>0:r1=0; 2:r1=2; x=2; y=1;
Ok
Witnesses
Positive: 8, Negative: 319999992
Condition exists (x=2 /\ y=2 /\ 0:r1=2 /\ 2:r1=2) is validated
Hash=3ff9f33d19c19af532626ad01e67e950
Cycle=DpdW Wse Rfe DpdW Wse Rfe
Relax rfe004 Ok Rfe
Safe=Wse DpdW
Time rfe004 77.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: li 7,1
_litmus_P3_1_: stw 7,0(9)
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: li 8,2
_litmus_P1_1_: stw 8,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 4,3,3
_litmus_P0_2_: li 10,1
_litmus_P0_3_: stwx 10,4,9
Test rfe005 Allowed
Histogram (24 states)
6 :>0:r1=1; 2:r1=2; 2:r4=0; y=2;
12 :>0:r1=1; 2:r1=1; 2:r4=0; y=1;
14 :>0:r1=1; 2:r1=1; 2:r4=0; y=2;
80044 :>0:r1=0; 2:r1=0; 2:r4=1; y=1;
238612:>0:r1=0; 2:r1=0; 2:r4=1; y=2;
2095330:>0:r1=0; 2:r1=2; 2:r4=1; y=1;
15891285:>0:r1=0; 2:r1=1; 2:r4=1; y=2;
20559376:>0:r1=0; 2:r1=1; 2:r4=0; y=2;
7828722:>0:r1=0; 2:r1=1; 2:r4=0; y=1;
15572036:>0:r1=0; 2:r1=2; 2:r4=0; y=1;
5442951:>0:r1=1; 2:r1=1; 2:r4=1; y=2;
5364529:>0:r1=1; 2:r1=0; 2:r4=0; y=2;
9542353:>0:r1=0; 2:r1=2; 2:r4=0; y=2;
14124253:>0:r1=1; 2:r1=0; 2:r4=1; y=2;
30364736:>0:r1=1; 2:r1=0; 2:r4=0; y=1;
7525370:>0:r1=1; 2:r1=2; 2:r4=1; y=2;
19519255:>0:r1=0; 2:r1=1; 2:r4=1; y=1;
21704401:>0:r1=1; 2:r1=0; 2:r4=1; y=1;
26204772:>0:r1=0; 2:r1=0; 2:r4=0; y=2;
7740822:>0:r1=1; 2:r1=2; 2:r4=0; y=1;
19948858:>0:r1=1; 2:r1=1; 2:r4=1; y=1;
18096076:>0:r1=0; 2:r1=0; 2:r4=0; y=1;
31547918:>0:r1=0; 2:r1=2; 2:r4=1; y=2;
40608269:>0:r1=1; 2:r1=2; 2:r4=1; y=1;
Ok
Witnesses
Positive: 6, Negative: 319999994
Condition exists (y=2 /\ 0:r1=1 /\ 2:r1=2 /\ 2:r4=0) is validated
Hash=38f61d39ea6d477ceb57de4910657abe
Cycle=DpdR Fre Rfe DpdW Wse Rfe
Relax rfe005 Ok Rfe
Safe=Fre Wse DpdW DpdR
Time rfe005 78.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: li 7,1
_litmus_P3_1_: stw 7,0(9)
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 31,10,9
Test rfe006 Allowed
Histogram (16 states)
29 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=0;
32269 :>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1;
22722192:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0;
8576797:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0;
20024805:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1;
7845032:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0;
20157322:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1;
53107243:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0;
7689962:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0;
22709778:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1;
15038558:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1;
29145487:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0;
29368570:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1;
15373368:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0;
59641028:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1;
8567560:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1;
Ok
Witnesses
Positive: 29, Negative: 319999971
Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is validated
Hash=8352ce27483f00d649cb0bf6b7f9ba8b
Cycle=DpdR Fre Rfe DpdR Fre Rfe
Relax rfe006 Ok Rfe
Safe=Fre DpdR
Time rfe006 77.31
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Fri Dec 18 16:31:00 GMT 2009