Thu Dec 31 09:32:57 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwsrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwsrr000
"DpdR Fre SyncdWW Wse Rfe LwSyncsRR"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r6=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | | lwz r3,0(r2) ;
li r3,1 | | xor r4,r3,r3 ;
stw r3,0(r4) | | lwzx r5,r4,r6 ;
exists (y=2 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=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_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r4,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r5,0(r9)
_litmus_P2_3_: xor r10,r5,r5
_litmus_P2_4_: lwzx r11,r10,r2
Test aclwsrr000 Allowed
Histogram (16 states)
33 :>2:r1=1; 2:r3=2; 2:r5=1; y=2;
76 :>2:r1=0; 2:r3=1; 2:r5=1; y=2;
182 :>2:r1=0; 2:r3=2; 2:r5=0; y=1;
27119 :>2:r1=0; 2:r3=0; 2:r5=0; y=2;
228 :>2:r1=0; 2:r3=2; 2:r5=1; y=2;
510 :>2:r1=2; 2:r3=1; 2:r5=1; y=1;
4331 :>2:r1=0; 2:r3=2; 2:r5=1; y=1;
4089 :>2:r1=0; 2:r3=1; 2:r5=1; y=1;
3868151:>2:r1=2; 2:r3=2; 2:r5=0; y=1;
1369303:>2:r1=1; 2:r3=1; 2:r5=1; y=2;
1086978:>2:r1=2; 2:r3=2; 2:r5=1; y=2;
2392286:>2:r1=0; 2:r3=0; 2:r5=1; y=2;
11136915:>2:r1=2; 2:r3=2; 2:r5=1; y=1;
3675308:>2:r1=0; 2:r3=0; 2:r5=1; y=1;
3801606:>2:r1=1; 2:r3=1; 2:r5=1; y=1;
12632885:>2:r1=0; 2:r3=0; 2:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=0e168a11add8ac7b91db489d5c03a6a4
Cycle=DpdR Fre SyncdWW Wse Rfe LwSyncsRR
Relax aclwsrr000 No ACLwSyncsRR
Safe=Fre Wse SyncdWW DpdR
Time aclwsrr000 74.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwsrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwsrr001
"DpdR Fre SyncdWW Rfe LwSyncsRR Fre Rfe LwSyncsRR"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 3:r2=y; 3:r6=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r2) | | lwz r3,0(r2) ;
li r3,1 | | | xor r4,r3,r3 ;
stw r3,0(r4) | | | lwzx r5,r4,r6 ;
exists (y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=2 /\ 3:r5=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 r8,0(r2)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r9,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r4,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r5,0(r9)
_litmus_P3_3_: xor r10,r5,r5
_litmus_P3_4_: lwzx r11,r10,r2
Test aclwsrr001 Allowed
Histogram (88 states)
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
3 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
7 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
2 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
9 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
8 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
4 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
15 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
23 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
11 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
185 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
90 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
66 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
57 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
7 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
81 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
1608 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
33 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1642 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
42 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
51 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
13740 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
672 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
319 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
2474 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
2 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
7869 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
27331 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
117 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
155503:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
745 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
1974 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1999 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
6077 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
163 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
139 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
665 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
7415 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
5498 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
518 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
11625 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
14944 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
1020 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
866 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
1254 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
21256 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
11649 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
233 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
2170 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
2912 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
328 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
33640 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
4500 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
8802 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
1631 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
1075 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
24609 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
875 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
4066 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
143529:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
22461 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
72956 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
109236:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
11892 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
7421 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
132724:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
49421 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
1084544:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
140479:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
62798 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
1018197:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
877717:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
775127:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
390979:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
674015:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
1150994:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1305854:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
7008881:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
2374051:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
447908:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
2819923:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
381703:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
4411168:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
4552813:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
6587957:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
1875695:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
1124933:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=2 /\ 3:r5=0) is NOT validated
Hash=c675ca6562f64b0057e406348aad3876
Cycle=DpdR Fre SyncdWW Rfe LwSyncsRR Fre Rfe LwSyncsRR
Relax aclwsrr001 No ACLwSyncsRR
Safe=Fre SyncdWW DpdR
Time aclwsrr001 197.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwsrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwsrr002
"DpdR Fre Rfe LwSyncsRR DpdR Fre Rfe LwSyncsRR"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r6=x; 3:r2=x;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
lwsync | stw r1,0(r2) | lwsync | 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:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 2:r1=1 /\ 2:r3=1 /\ 2:r5=0)
Generated assembler
_litmus_P0_0_: lwz r4,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r5,0(r9)
_litmus_P0_3_: xor r10,r5,r5
_litmus_P0_4_: lwzx r11,r10,r2
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r4,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r5,0(r9)
_litmus_P2_3_: xor r10,r5,r5
_litmus_P2_4_: lwzx r11,r10,r2
_litmus_P3_0_: li r9,1
_litmus_P3_1_: stw r9,0(r2)
Test aclwsrr002 Allowed
Histogram (31 states)
1 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
230 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
456 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
642 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
51 :>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
262 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=0;
133 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
8403 :>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
162 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
11067 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
35033 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
6518 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
225590:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
110266:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
114484:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
95195 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=0;
41652 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
7343 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
85254 :>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
170117:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
2423964:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
3687514:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
152536:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
1280726:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
482173:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
4382902:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
4770710:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
15046079:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
2624547:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
3697700:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
538290:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 2:r1=1 /\ 2:r3=1 /\ 2:r5=0) is NOT validated
Hash=050ce9f57369bcd60ead287482f2d6b6
Cycle=DpdR Fre Rfe LwSyncsRR DpdR Fre Rfe LwSyncsRR
Relax aclwsrr002 No ACLwSyncsRR
Safe=Fre DpdR
Time aclwsrr002 95.92
$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: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 40
Thu Dec 31 09:39:05 CET 2009