Fri Dec 18 15:53:30 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfi000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfi000
"DpdR Fre Rfi DpdR Fre Rfi"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | li r1,1 ;
stw r1,0(r2) | stw r1,0(r2) ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: li 10,1
_litmus_P1_1_: stw 10,0(11)
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 31,8,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 31,8,9
Test rfi000 Allowed
Histogram (4 states)
15 :>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0;
78 :>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1;
1999951:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1;
1999956:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0;
Ok
Witnesses
Positive: 15, Negative: 3999985
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 1:r5=0) is validated
Hash=ae5383af5602499e3f412f54983b391a
Cycle=DpdR Fre Rfi DpdR Fre Rfi
Relax rfi000 Ok Rfi
Safe=Fre DpdR
Time rfi000 2.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfi001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfi001
"DpdW Wse Rfi DpdR Fre Rfi"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,2 | li r1,1 ;
stw r1,0(r2) | stw r1,0(r2) ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | li r5,1 ;
| stwx r5,r4,r6 ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r3=1)
Generated assembler
_litmus_P1_0_: li 31,1
_litmus_P1_1_: stw 31,0(11)
_litmus_P1_2_: lwz 3,0(11)
_litmus_P1_3_: xor 10,3,3
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stwx 8,10,9
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 31,8,9
Test rfi001 Allowed
Histogram (5 states)
4 :>0:r3=1; 0:r5=1; 1:r3=1; x=1;
719 :>0:r3=2; 0:r5=1; 1:r3=1; x=1;
2848 :>0:r3=2; 0:r5=0; 1:r3=1; x=2;
2000045:>0:r3=2; 0:r5=0; 1:r3=1; x=1;
1996384:>0:r3=2; 0:r5=1; 1:r3=1; x=2;
Ok
Witnesses
Positive: 2848, Negative: 3997152
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r3=1) is validated
Hash=1214f5a1e6438b4c5396ac2ff0d9c78b
Cycle=DpdW Wse Rfi DpdR Fre Rfi
Relax rfi001 Ok Rfi
Safe=Fre Wse DpdW DpdR
Time rfi001 2.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/rfi002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
rfi002
"DpdW Wse Rfi DpdW Wse Rfi"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
li r5,1 | li r5,1 ;
stwx r5,r4,r6 | stwx r5,r4,r6 ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 1:r3=2)
Generated assembler
_litmus_P1_0_: li 31,2
_litmus_P1_1_: stw 31,0(11)
_litmus_P1_2_: lwz 3,0(11)
_litmus_P1_3_: xor 10,3,3
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stwx 8,10,9
_litmus_P0_0_: li 31,2
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: lwz 3,0(11)
_litmus_P0_3_: xor 10,3,3
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stwx 8,10,9
Test rfi002 Allowed
Histogram (6 states)
13 :>0:r3=2; 1:r3=1; x=1; y=1;
46 :>0:r3=1; 1:r3=2; x=1; y=1;
46521 :>0:r3=2; 1:r3=2; x=1; y=1;
7286 :>0:r3=2; 1:r3=2; x=2; y=2;
1938067:>0:r3=2; 1:r3=2; x=1; y=2;
2008067:>0:r3=2; 1:r3=2; x=2; y=1;
Ok
Witnesses
Positive: 7286, Negative: 3992714
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 1:r3=2) is validated
Hash=e591671895bcc80990ce95bcf97254d5
Cycle=DpdW Wse Rfi DpdW Wse Rfi
Relax rfi002 Ok Rfi
Safe=Wse DpdW
Time rfi002 2.20
$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=-a 0 -r 2000
Fri Dec 18 15:53:38 GMT 2009