[Agda] 5 sec performance gain on std-lib
James Chapman
james at cs.ioc.ee
Fri Oct 19 14:16:50 CEST 2012
Inconclusive!
OS X 10.8.2, ghc 7.4.1 (32-bit)
=======================
Before:
62,117,743,772 bytes allocated in the heap
14,420,702,632 bytes copied during GC
175,975,880 bytes maximum residency (101 sample(s))
2,991,320 bytes maximum slop
508 MB total memory in use (0 MB lost due to fragmentation)
Tot time (elapsed) Avg pause Max pause
Gen 0 118621 colls, 0 par 27.66s 27.85s 0.0002s 0.0052s
Gen 1 101 colls, 0 par 15.75s 15.98s 0.1582s 0.4894s
INIT time 0.00s ( 0.00s elapsed)
MUT time 91.65s ( 95.64s elapsed)
GC time 43.41s ( 43.83s elapsed)
EXIT time 0.00s ( 0.00s elapsed)
Total time 135.07s (139.47s elapsed)
%GC time 32.1% (31.4% elapsed)
Alloc rate 677,664,338 bytes per MUT second
Productivity 67.9% of total user, 65.7% of total elapsed
real 2m19.542s
user 2m15.071s
sys 0m0.993s
After:
62,190,015,688 bytes allocated in the heap
14,513,546,744 bytes copied during GC
210,122,632 bytes maximum residency (101 sample(s))
2,594,868 bytes maximum slop
570 MB total memory in use (0 MB lost due to fragmentation)
Tot time (elapsed) Avg pause Max pause
Gen 0 118760 colls, 0 par 27.54s 27.72s 0.0002s 0.0040s
Gen 1 101 colls, 0 par 16.13s 16.37s 0.1621s 0.5675s
INIT time 0.00s ( 0.00s elapsed)
MUT time 90.76s ( 91.31s elapsed)
GC time 43.67s ( 44.09s elapsed)
EXIT time 0.00s ( 0.00s elapsed)
Total time 134.45s (135.40s elapsed)
%GC time 32.5% (32.6% elapsed)
Alloc rate 685,106,273 bytes per MUT second
Productivity 67.5% of total user, 67.0% of total elapsed
real 2m15.471s
user 2m14.446s
sys 0m0.961s
Debian Squeeze, ghc 6.12.1 (64-bit)
============================
Before:
153,193,142,288 bytes allocated in the heap
40,299,501,176 bytes copied during GC
426,795,464 bytes maximum residency (141 sample(s))
10,529,848 bytes maximum slop
1118 MB total memory in use (17 MB lost due to fragmentation)
Generation 0: 291395 collections, 0 parallel, 186.92s, 189.36s elapsed
Generation 1: 141 collections, 0 parallel, 66.61s, 67.98s elapsed
INIT time 0.00s ( 0.00s elapsed)
MUT time 317.52s (322.11s elapsed)
GC time 253.53s (257.34s elapsed)
EXIT time 0.00s ( 0.00s elapsed)
Total time 571.06s (579.45s elapsed)
%GC time 44.4% (44.4% elapsed)
Alloc rate 482,461,785 bytes per MUT second
Productivity 55.6% of total user, 54.8% of total elapsed
real 9m39.626s
user 9m31.056s
sys 0m4.280s
After:
153,398,268,928 bytes allocated in the heap
40,331,707,952 bytes copied during GC
426,772,136 bytes maximum residency (141 sample(s))
10,679,392 bytes maximum slop
1118 MB total memory in use (17 MB lost due to fragmentation)
Generation 0: 291786 collections, 0 parallel, 166.29s, 168.08s elapsed
Generation 1: 141 collections, 0 parallel, 65.15s, 66.50s elapsed
INIT time 0.00s ( 0.00s elapsed)
MUT time 315.70s (319.09s elapsed)
GC time 231.43s (234.58s elapsed)
EXIT time 0.00s ( 0.00s elapsed)
Total time 547.13s (553.67s elapsed)
%GC time 42.3% (42.4% elapsed)
Alloc rate 485,899,239 bytes per MUT second
Productivity 57.7% of total user, 57.0% of total elapsed
real 9m13.860s
user 9m7.134s
sys 0m4.276s
On Oct 19, 2012, at 3:15 PM, James Chapman <jmchapman at gmail.com> wrote:
> Inconclusive!
>
> OS X 10.8.2, ghc 7.4.1 (32-bit)
> =======================
>
> Before:
> 62,117,743,772 bytes allocated in the heap
> 14,420,702,632 bytes copied during GC
> 175,975,880 bytes maximum residency (101 sample(s))
> 2,991,320 bytes maximum slop
> 508 MB total memory in use (0 MB lost due to fragmentation)
>
> Tot time (elapsed) Avg pause Max pause
> Gen 0 118621 colls, 0 par 27.66s 27.85s 0.0002s 0.0052s
> Gen 1 101 colls, 0 par 15.75s 15.98s 0.1582s 0.4894s
>
> INIT time 0.00s ( 0.00s elapsed)
> MUT time 91.65s ( 95.64s elapsed)
> GC time 43.41s ( 43.83s elapsed)
> EXIT time 0.00s ( 0.00s elapsed)
> Total time 135.07s (139.47s elapsed)
>
> %GC time 32.1% (31.4% elapsed)
>
> Alloc rate 677,664,338 bytes per MUT second
>
> Productivity 67.9% of total user, 65.7% of total elapsed
>
>
> real 2m19.542s
> user 2m15.071s
> sys 0m0.993s
>
>
> After:
> 62,190,015,688 bytes allocated in the heap
> 14,513,546,744 bytes copied during GC
> 210,122,632 bytes maximum residency (101 sample(s))
> 2,594,868 bytes maximum slop
> 570 MB total memory in use (0 MB lost due to fragmentation)
>
> Tot time (elapsed) Avg pause Max pause
> Gen 0 118760 colls, 0 par 27.54s 27.72s 0.0002s 0.0040s
> Gen 1 101 colls, 0 par 16.13s 16.37s 0.1621s 0.5675s
>
> INIT time 0.00s ( 0.00s elapsed)
> MUT time 90.76s ( 91.31s elapsed)
> GC time 43.67s ( 44.09s elapsed)
> EXIT time 0.00s ( 0.00s elapsed)
> Total time 134.45s (135.40s elapsed)
>
> %GC time 32.5% (32.6% elapsed)
>
> Alloc rate 685,106,273 bytes per MUT second
>
> Productivity 67.5% of total user, 67.0% of total elapsed
>
>
> real 2m15.471s
> user 2m14.446s
> sys 0m0.961s
>
>
> Debian Squeeze, ghc 6.12.1 (64-bit)
> ============================
> Before:
> 153,193,142,288 bytes allocated in the heap
> 40,299,501,176 bytes copied during GC
> 426,795,464 bytes maximum residency (141 sample(s))
> 10,529,848 bytes maximum slop
> 1118 MB total memory in use (17 MB lost due to fragmentation)
>
> Generation 0: 291395 collections, 0 parallel, 186.92s, 189.36s elapsed
> Generation 1: 141 collections, 0 parallel, 66.61s, 67.98s elapsed
>
> INIT time 0.00s ( 0.00s elapsed)
> MUT time 317.52s (322.11s elapsed)
> GC time 253.53s (257.34s elapsed)
> EXIT time 0.00s ( 0.00s elapsed)
> Total time 571.06s (579.45s elapsed)
>
> %GC time 44.4% (44.4% elapsed)
>
> Alloc rate 482,461,785 bytes per MUT second
>
> Productivity 55.6% of total user, 54.8% of total elapsed
>
>
> real 9m39.626s
> user 9m31.056s
> sys 0m4.280s
>
> After:
> 153,398,268,928 bytes allocated in the heap
> 40,331,707,952 bytes copied during GC
> 426,772,136 bytes maximum residency (141 sample(s))
> 10,679,392 bytes maximum slop
> 1118 MB total memory in use (17 MB lost due to fragmentation)
>
> Generation 0: 291786 collections, 0 parallel, 166.29s, 168.08s elapsed
> Generation 1: 141 collections, 0 parallel, 65.15s, 66.50s elapsed
>
> INIT time 0.00s ( 0.00s elapsed)
> MUT time 315.70s (319.09s elapsed)
> GC time 231.43s (234.58s elapsed)
> EXIT time 0.00s ( 0.00s elapsed)
> Total time 547.13s (553.67s elapsed)
>
> %GC time 42.3% (42.4% elapsed)
>
> Alloc rate 485,899,239 bytes per MUT second
>
> Productivity 57.7% of total user, 57.0% of total elapsed
>
>
> real 9m13.860s
> user 9m7.134s
> sys 0m4.276s
>
>
>
> On Oct 19, 2012, at 2:32 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>
>> Hi folks,
>>
>> it seems that I have won 5 seconds on the library-test by some seemingly irrelevant optimizations in the termination checker. Can someone verify?
>>
>> Patch is upstream:
>>
>> Fri Oct 19 09:36:45 CEST 2012 Andreas Abel <andreas.abel at ifi.lmu.de>
>> * Some refactoring in the comparison of call arguments to formal parameters.
>> Do not cut off order relations at this phase.
>>
>> If that is the case, some more fumbling with the termination checker could pay off.
>>
>> Cheers,
>> Andreas
>>
>> --
>> Andreas Abel <>< Du bist der geliebte Mensch.
>>
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>>
>> andreas.abel at ifi.lmu.de
>> http://www2.tcs.ifi.lmu.de/~abel/
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
More information about the Agda
mailing list