Tue Jan 5 18:06:16 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)
6131359:>2:r1=0; 2:r3=0; 2:r5=0; y=1;
1560 :>2:r1=0; 2:r3=2; 2:r5=0; y=1;
1728165:>2:r1=2; 2:r3=2; 2:r5=0; y=1;
184823:>2:r1=0; 2:r3=0; 2:r5=1; y=1;
104404:>2:r1=0; 2:r3=1; 2:r5=1; y=1;
1679455:>2:r1=1; 2:r3=1; 2:r5=1; y=1;
176005:>2:r1=2; 2:r3=1; 2:r5=1; y=1;
56581 :>2:r1=0; 2:r3=2; 2:r5=1; y=1;
3884730:>2:r1=2; 2:r3=2; 2:r5=1; y=1;
534082:>2:r1=0; 2:r3=0; 2:r5=0; y=2;
1120110:>2:r1=0; 2:r3=0; 2:r5=1; y=2;
12313 :>2:r1=0; 2:r3=1; 2:r5=1; y=2;
1074666:>2:r1=1; 2:r3=1; 2:r5=1; y=2;
41031 :>2:r1=0; 2:r3=2; 2:r5=1; y=2;
2809 :>2:r1=1; 2:r3=2; 2:r5=1; y=2;
3267907:>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 19.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (95 states)
3380176:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
28829 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
527048:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
284 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
56367 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
1871295:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
69342 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
29 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
1 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
35 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
2102 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
576332:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
48 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
68148 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
885 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1694 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1517026:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
169461:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
5559 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
38237 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
9 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1235 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
15884 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
162793:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
586 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
48681 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
79 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
190 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
10651 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
651335:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
23768 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
819912:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
12223 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
4357 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
683854:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
8323 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
184 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
41873 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
197 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
53 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
35623 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
169782:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
140 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
4997 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
5 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
303 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
12403 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
1067017:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
4809 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
598886:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
4062 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
6257 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
2006347:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
528004:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
170 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
40075 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
1604 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
13 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
16612 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
740071:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
5877 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
303046:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
19571 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
7335 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
369024:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
22694 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
172 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
14990 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
45 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
12 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
2379 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
422890:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
5562 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
511278:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
8223 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
5190 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
216811:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
78304 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
152 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
15156 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
716 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
64 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
40033 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
9291 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
12 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
10365 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
158 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
3 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
11462 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
604216:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
2274 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
375669:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
22246 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
3780 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
874735:>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 24.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2009425:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
74751 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
578043:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
887545:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
205517:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
2338393:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
22747 :>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=0;
1001 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
213 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
151 :>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
447214:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=0;
935264:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
84839 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
251620:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
1102740:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
2621 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
916041:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
169 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
3757 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
1092848:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
217057:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
48 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
55975 :>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
1552 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
5796 :>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
625967:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
2103368:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
1111 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
206744:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
873938:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
675122:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
4278423:>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 20.27
$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=-s 1000 -r 20000
Tue Jan 5 18:07:21 CET 2010