[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