Fri Dec 18 16:25:02 CET 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_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwz r5,0(r9)
_litmus_P0_3_: xor r11,r5,r5
_litmus_P0_4_: lwzx r6,r11,r2
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwz r5,0(r9)
_litmus_P1_3_: xor r11,r5,r5
_litmus_P1_4_: lwzx r6,r11,r2
Test rfi000 Allowed
Histogram (4 states)
388 :>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=0;
40971 :>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=1;
978137:>0:r3=1; 0:r5=0; 1:r3=1; 1:r5=1;
980504:>0:r3=1; 0:r5=1; 1:r3=1; 1:r5=0;
Ok
Witnesses
Positive: 388, Negative: 1999612
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 1.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwz r5,0(r9)
_litmus_P0_3_: xor r11,r5,r5
_litmus_P0_4_: lwzx r6,r11,r2
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwz r6,0(r9)
_litmus_P1_3_: xor r11,r6,r6
_litmus_P1_4_: li r7,1
_litmus_P1_5_: stwx r7,r11,r2
Test rfi001 Allowed
Histogram (5 states)
140 :>0:r3=2; 0:r5=0; 1:r3=1; x=2;
1419 :>0:r3=1; 0:r5=1; 1:r3=1; x=1;
914415:>0:r3=2; 0:r5=0; 1:r3=1; x=1;
965462:>0:r3=2; 0:r5=1; 1:r3=1; x=2;
118564:>0:r3=2; 0:r5=1; 1:r3=1; x=1;
Ok
Witnesses
Positive: 140, Negative: 1999860
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 1.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,2
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwz r6,0(r9)
_litmus_P0_3_: xor r11,r6,r6
_litmus_P0_4_: li r7,1
_litmus_P0_5_: stwx r7,r11,r2
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: lwz r6,0(r9)
_litmus_P1_3_: xor r11,r6,r6
_litmus_P1_4_: li r7,1
_litmus_P1_5_: stwx r7,r11,r2
Test rfi002 Allowed
Histogram (6 states)
3 :>0:r3=1; 1:r3=2; x=1; y=1;
7 :>0:r3=2; 1:r3=1; x=1; y=1;
1133 :>0:r3=2; 1:r3=2; x=2; y=2;
900000:>0:r3=2; 1:r3=2; x=1; y=2;
919926:>0:r3=2; 1:r3=2; x=2; y=1;
178931:>0:r3=2; 1:r3=2; x=1; y=1;
Ok
Witnesses
Positive: 1133, Negative: 1998867
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 1.27
$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=
Fri Dec 18 16:25:06 CET 2009