Fri Jan 1 17:49:35 CET 2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
98 :>2:r1=0; 2:r3=1; 2:r5=1; y=2;
97 :>2:r1=1; 2:r3=2; 2:r5=1; y=2;
56943 :>2:r1=0; 2:r3=0; 2:r5=0; y=2;
8093 :>2:r1=0; 2:r3=1; 2:r5=1; y=1;
518 :>2:r1=0; 2:r3=2; 2:r5=1; y=2;
1107 :>2:r1=2; 2:r3=1; 2:r5=1; y=1;
10094879:>2:r1=2; 2:r3=2; 2:r5=0; y=1;
8131 :>2:r1=0; 2:r3=2; 2:r5=1; y=1;
4569419:>2:r1=0; 2:r3=0; 2:r5=1; y=2;
2134359:>2:r1=2; 2:r3=2; 2:r5=1; y=2;
2505478:>2:r1=1; 2:r3=1; 2:r5=1; y=2;
25219819:>2:r1=0; 2:r3=0; 2:r5=0; y=1;
7541133:>2:r1=1; 2:r3=1; 2:r5=1; y=1;
20828903:>2:r1=2; 2:r3=2; 2:r5=1; y=1;
7030669:>2:r1=0; 2:r3=0; 2:r5=1; y=1;
354 :>2:r1=0; 2:r3=2; 2:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 143.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (91 states)
1 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
2 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
2 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
7 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
9 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
4 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
10 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
11 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
6 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
21 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
27 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
238 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
356 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
97 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
33 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
71 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
13 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
83 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
172 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
245 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
8 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
516 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1615 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
25445 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
240134:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
33121 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
3333 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
3268 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
794 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
17761 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
42242 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
1299 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
4317 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
50 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
1445 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
290 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
2304 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
27602 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
1293 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
166 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1509 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
954 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
9143 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
13667 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
44385 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
9324 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
246 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
50812 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
1829 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
3461 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
31305 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
183838:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
2123 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
3365 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
7299 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
105050:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
8574 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
56217 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
173 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
1197 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
6027 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
18893 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
3944 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
260829:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
172551:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
20654 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
16084 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
12688 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
415440:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
360950:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
863875:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
1704163:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
296746:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
1919783:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
1958371:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
2353132:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
790449:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1584232:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
1445588:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
4630571:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
6147948:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
770100:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
8888847:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
13432671:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
2238779:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
9581633:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
2135781:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
3232753:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
13793634:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 405.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (32 states)
3 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
2 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
136 :>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
406 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
346 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
309 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
1425 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
826 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
13474 :>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
488 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=0;
20165 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
12301 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
175615:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
12586 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
87847 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
445385:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
68450 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
297363:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
1021368:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
1025338:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
213275:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
9465404:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
8708986:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
376466:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
2359420:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
290973:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
236343:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=0;
4589884:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
7416533:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
7475077:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
5097464:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
30586342:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 200.55
$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 80
Fri Jan 1 18:02:05 CET 2010