Tue Dec 29 15:27:06 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 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_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r10,0(r9)
_litmus_P2_3_: xor r7,r10,r10
_litmus_P2_4_: lwzx r8,r7,r2
Test aclwsrr000 Allowed
Histogram (16 states)
1549 :>2:r1=1; 2:r3=2; 2:r5=1; y=2;
502 :>2:r1=0; 2:r3=1; 2:r5=1; y=2;
42905 :>2:r1=0; 2:r3=0; 2:r5=0; y=2;
18000 :>2:r1=0; 2:r3=2; 2:r5=1; y=2;
973 :>2:r1=0; 2:r3=2; 2:r5=0; y=1;
19230 :>2:r1=0; 2:r3=1; 2:r5=1; y=1;
57529 :>2:r1=2; 2:r3=1; 2:r5=1; y=1;
744152:>2:r1=2; 2:r3=2; 2:r5=1; y=2;
4321301:>2:r1=2; 2:r3=2; 2:r5=0; y=1;
9711 :>2:r1=0; 2:r3=2; 2:r5=1; y=1;
720226:>2:r1=1; 2:r3=1; 2:r5=1; y=2;
2916284:>2:r1=0; 2:r3=0; 2:r5=1; y=2;
11447647:>2:r1=2; 2:r3=2; 2:r5=1; y=1;
3289329:>2:r1=0; 2:r3=0; 2:r5=1; y=1;
3392277:>2:r1=1; 2:r3=1; 2:r5=1; y=1;
13018385:>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 40.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,0(r2)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r11,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r9)
_litmus_P3_3_: xor r7,r10,r10
_litmus_P3_4_: lwzx r8,r7,r2
Test aclwsrr001 Allowed
Histogram (95 states)
3 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
1 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
2 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
15 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
3 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
2 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
8 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
1 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
8 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
2 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
12 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
3 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
29 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
10 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
93 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
358 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
19 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
139 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
16 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
1019 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
2 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
30 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
29 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
504 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
377 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1235 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
856 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
73 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
30 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
196 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
2503 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
336 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
403 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
492 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
3688 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
1396 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
1317 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
8192 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
147 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
1965 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
1261 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
5146 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
6237 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
1104 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
692 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1556 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1305 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
4715 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
1477 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
3262 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
19224 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
1644 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
23918 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
2159 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
6388 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
7383 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
1729 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
135879:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
4017 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
1628 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
3503 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
72555 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
23047 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
941021:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
4461 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
3000205:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
332353:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
4670 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
161082:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
21779 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
824903:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
184332:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
922258:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
3563 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
635860:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
336621:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1290581:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
51713 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
4956012:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
890475:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
298124:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
210946:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
544596:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
405641:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
116423:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
5110208:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
6791300:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
583299:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
6520668:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
847031:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
1714415:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
352500:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
1587615:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
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 67.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r11,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r10,0(r9)
_litmus_P0_3_: xor r7,r10,r10
_litmus_P0_4_: lwzx r8,r7,r2
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r10,0(r9)
_litmus_P2_3_: xor r7,r10,r10
_litmus_P2_4_: lwzx r8,r7,r2
_litmus_P3_0_: li r9,1
_litmus_P3_1_: stw r9,0(r2)
Test aclwsrr002 Allowed
Histogram (32 states)
2 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
1 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
22 :>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
3398 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
1089 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
91 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
446 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
397 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
584 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=0;
14087 :>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
61187 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
31431 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
330490:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
44747 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=0;
102900:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
31116 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
92461 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
14654 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
79840 :>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
1731546:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
554947:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
3106612:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
103598:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
407819:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
601191:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
3135164:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
535448:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
5028188:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
5480957:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
2966263:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
2644426:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
12894898:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 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 47.28
$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 -O2 */
/* 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 -O2"
LITMUSOPTS=-r 40
Tue Dec 29 15:29:41 CET 2009