Sat Dec 26 14:44:16 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/posrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr003
"DpdR Fre SyncdWW Rfe DpdR PosRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 1:r9=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
li r3,1 | lwz r6,0(r5) ;
stw r3,0(r4) | xor r7,r6,r6 ;
| lwzx r8,r7,r9 ;
exists (1:r1=1 /\ 1:r8=0)
Generated assembler
_litmus_P1_0_: lwz 25,0(10)
_litmus_P1_1_: xor 27,25,25
_litmus_P1_2_: lwzx 8,27,11
_litmus_P1_3_: lwz 7,0(11)
_litmus_P1_4_: xor 6,7,7
_litmus_P1_5_: lwzx 26,6,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test posrr003 Allowed
Histogram (4 states)
2 :>1:r1=1; 1:r8=0;
4904814:>1:r1=0; 1:r8=1;
15095145:>1:r1=1; 1:r8=1;
20000039:>1:r1=0; 1:r8=0;
Ok
Witnesses
Positive: 2, Negative: 39999998
Condition exists (1:r1=1 /\ 1:r8=0) is validated
Hash=b660291ec0b800081e710e7f87d96ef9
Cycle=DpdR Fre SyncdWW Rfe DpdR PosRR
Relax posrr003 Ok PosRR
Safe=Fre DpdR BCSyncdWW
Time posrr003 31.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/posrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr005
"DpdR Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=a; 2:r9=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | xor r3,r1,r1 ;
sync | li r3,1 | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | lwz r6,0(r5) ;
stw r3,0(r4) | | xor r7,r6,r6 ;
| | lwzx r8,r7,r9 ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r8=0)
Generated assembler
_litmus_P2_0_: lwz 24,0(10)
_litmus_P2_1_: xor 26,24,24
_litmus_P2_2_: lwzx 8,26,11
_litmus_P2_3_: lwz 7,0(11)
_litmus_P2_4_: xor 6,7,7
_litmus_P2_5_: lwzx 25,6,9
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test posrr005 Allowed
Histogram (8 states)
1 :>1:r1=1; 2:r1=1; 2:r8=0;
1916619:>1:r1=0; 2:r1=0; 2:r8=1;
4545677:>1:r1=0; 2:r1=1; 2:r8=0;
1535249:>1:r1=1; 2:r1=0; 2:r8=0;
337785:>1:r1=1; 2:r1=1; 2:r8=1;
14210017:>1:r1=0; 2:r1=0; 2:r8=0;
7204335:>1:r1=1; 2:r1=0; 2:r8=1;
10250317:>1:r1=0; 2:r1=1; 2:r8=1;
Ok
Witnesses
Positive: 1, Negative: 39999999
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r8=0) is validated
Hash=8d0831339733254b3c8a1735bb7650c7
Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR
Relax posrr005 Ok PosRR
Safe=Fre DpdR BCSyncdWW BCSyncdRW
Time posrr005 47.71
$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
Sat Dec 26 14:45:35 GMT 2009