Mon Dec 28 11:29:26 CET 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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r3,0(r11)
_litmus_P1_1_: xor r7,r3,r3
_litmus_P1_2_: lwzx r10,r7,r9
_litmus_P1_3_: lwz r8,0(r9)
_litmus_P1_4_: xor r29,r8,r8
_litmus_P1_5_: lwzx r4,r29,r2
Test posrr003 Allowed
Histogram (4 states)
3 :>1:r1=1; 1:r8=0;
141347:>1:r1=0; 1:r8=0;
1073601:>1:r1=0; 1:r8=1;
785049:>1:r1=1; 1:r8=1;
Ok
Witnesses
Positive: 3, Negative: 1999997
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 1.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r10,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stw r8,0(r2)
_litmus_P2_0_: lwz r29,0(r11)
_litmus_P2_1_: xor r7,r29,r29
_litmus_P2_2_: lwzx r10,r7,r9
_litmus_P2_3_: lwz r8,0(r9)
_litmus_P2_4_: xor r4,r8,r8
_litmus_P2_5_: lwzx r3,r4,r2
Test posrr005 Allowed
Histogram (7 states)
549 :>1:r1=1; 2:r1=0; 2:r8=0;
2533 :>1:r1=0; 2:r1=1; 2:r8=0;
4953 :>1:r1=1; 2:r1=1; 2:r8=1;
90642 :>1:r1=1; 2:r1=0; 2:r8=1;
123799:>1:r1=0; 2:r1=0; 2:r8=0;
530213:>1:r1=0; 2:r1=0; 2:r8=1;
247311:>1:r1=0; 2:r1=1; 2:r8=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r8=0) is NOT validated
Hash=8d0831339733254b3c8a1735bb7650c7
Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR
Relax posrr005 No PosRR
Safe=Fre DpdR BCSyncdWW BCSyncdRW
Time posrr005 1.74
$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=
Mon Dec 28 11:29:29 CET 2009