Mon Jan 4 13:46:47 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r23,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r24,0(r9)
_litmus_P2_3_: xor r10,r24,r24
_litmus_P2_4_: lwzx r11,r10,r2
Test aclwsrr000 Allowed
Histogram (16 states)
6447448:>2:r1=0; 2:r3=0; 2:r5=0; y=1;
161 :>2:r1=0; 2:r3=2; 2:r5=0; y=1;
1420103:>2:r1=2; 2:r3=2; 2:r5=0; y=1;
1592578:>2:r1=0; 2:r3=0; 2:r5=1; y=1;
14771 :>2:r1=0; 2:r3=1; 2:r5=1; y=1;
1433571:>2:r1=1; 2:r3=1; 2:r5=1; y=1;
68178 :>2:r1=2; 2:r3=1; 2:r5=1; y=1;
6259 :>2:r1=0; 2:r3=2; 2:r5=1; y=1;
6114285:>2:r1=2; 2:r3=2; 2:r5=1; y=1;
40208 :>2:r1=0; 2:r3=0; 2:r5=0; y=2;
1596936:>2:r1=0; 2:r3=0; 2:r5=1; y=2;
630 :>2:r1=0; 2:r3=1; 2:r5=1; y=2;
652837:>2:r1=1; 2:r3=1; 2:r5=1; y=2;
8801 :>2:r1=0; 2:r3=2; 2:r5=1; y=2;
501 :>2:r1=1; 2:r3=2; 2:r5=1; y=2;
602733:>2:r1=2; 2:r3=2; 2:r5=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 22.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r28,0(r2)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r9,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r24,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r25,0(r9)
_litmus_P3_3_: xor r10,r25,r25
_litmus_P3_4_: lwzx r11,r10,r2
Test aclwsrr001 Allowed
Histogram (88 states)
4135667:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
2700 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
64052 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
295 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
10126 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
1980391:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
49321 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
2 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
2 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
318 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
587618:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
25 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1211 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
95 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
178 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1582681:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1195782:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
2770 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
311022:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
363 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1454 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
197439:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
54033 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
6 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
8391 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
8 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
4108 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
341101:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
1152 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
671740:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
1540 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
109 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
336532:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
7953 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
1 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
6581 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
29 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
3 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
22244 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
197914:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
10 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
867 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
2 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
19 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
6480 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
1987957:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
843 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
263336:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
4068 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
1363 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
3351164:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
43638 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
14 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
385 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
44 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
326 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
651483:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
480 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
432705:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
3022 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
833 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
489594:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
1378 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
2108 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
172 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
380747:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
171 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
61188 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
366 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
73 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
33194 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
7132 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
7758 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
12 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
5 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
10162 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
495 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
22 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
1 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
21 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
385766:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
6 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
34711 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
786 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
54 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
58077 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 27.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r25,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r26,0(r9)
_litmus_P0_3_: xor r10,r26,r26
_litmus_P0_4_: lwzx r11,r10,r2
_litmus_P1_0_: li r6,1
_litmus_P1_1_: stw r6,0(r2)
_litmus_P2_0_: lwz r25,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r26,0(r9)
_litmus_P2_3_: xor r10,r26,r26
_litmus_P2_4_: lwzx r11,r10,r2
_litmus_P3_0_: li r5,1
_litmus_P3_1_: stw r5,0(r2)
Test aclwsrr002 Allowed
Histogram (32 states)
919215:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
3758 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
165660:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
1206080:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
29665 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
2708857:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
898 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=0;
179 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
5 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
33 :>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
50069 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=0;
307782:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
7562 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
60273 :>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
1601563:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
1653 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
401239:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
37764 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
11892 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
1409487:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
51053 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
5 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
19662 :>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
6039 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
219 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
538778:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
2812461:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
435 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
75981 :>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
1274161:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
397155:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
5900417:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 21.51
$Revision: 3228 $
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 -O */
/* 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 -O"
LITMUSOPTS=-r 20 -v
Mon Jan 4 13:47:59 CET 2010