[Agda-dev] agda: <<loop>>

[Andreas Abel]

Wolfram,

can you also try the maint-2.4.2 branch of the development version, 
which is the "stable" branch?

I am curious whether the lack of speedup has something to do with the 
Sharing facility (which is off on maint but on on master).

Thanks,
Andreas

On 12.03.2015 23:41, Wolfram Kahl wrote:
> Yesterday morning, Ulf declared Issue 1396 as fixed
>
>     https://code.google.com/p/agda/issues/detail?id=1396
>
> --- thanks a lot, Ulf!
>
> That motivated me to get a current development version,
> and try it on my developments.
>
> (Before I actually get to try it on my developments,
>   it appears that I need to find out exactly how
>   ``the treatment of operators has changed'',
>   and probably switch to the now steroids,
>   but that is not what I am writing about now.)
>
>
> For a long time, I have routinely linked Agda with -threaded,
> and used -N5 to get decent speed-ups on garbage collection
> on my six-core machines --- for the standard library,
> it still gave about 5 seconds speedup on the four-minute run,
> but for my larger developments, it was even more noticeable.
>
> This has now changed quite drastically:
> Checking the standard library with -N1 still takes close to four minutes:
>
>    INIT    time    0.00s  (  0.00s elapsed)
>    MUT     time  164.94s  (165.21s elapsed)
>    GC      time   62.08s  ( 62.17s elapsed)
>    EXIT    time    0.05s  (  0.05s elapsed)
>    Total   time  227.10s  (227.45s elapsed)
>
>    Alloc rate    1,136,580,628 bytes per MUT second
>
>    Productivity  72.7% of total user, 72.5% of total elapsed
>
> real    3m47.536s
> user    3m46.050s
> sys     0m1.120s
>
> But adding cores makes it take more than twice as long:
>
> -N2:
>
>    INIT    time    0.00s  (  0.00s elapsed)
>    MUT     time  459.35s  (459.98s elapsed)
>    GC      time  113.89s  ( 61.40s elapsed)
>    EXIT    time    0.05s  (  0.05s elapsed)
>    Total   time  573.31s  (521.46s elapsed)
>
>    Alloc rate    408,122,565 bytes per MUT second
>
>    Productivity  80.1% of total user, 88.1% of total elapsed
>
> real    8m41.544s
> user    9m6.380s
> sys     0m27.010s
>
> ---------------
>
>    -N4:
>
>    INIT    time    0.00s  (  0.00s elapsed)
>    MUT     time  455.09s  (455.01s elapsed)
>    GC      time  207.99s  ( 58.24s elapsed)
>    EXIT    time    0.06s  (  0.06s elapsed)
>    Total   time  663.16s  (513.33s elapsed)
>
>    Alloc rate    411,948,428 bytes per MUT second
>
>    Productivity  68.6% of total user, 88.7% of total elapsed
>
> real    8m33.420s
> user    9m38.720s
> sys     1m24.530s
>
>
>
> This looks a bit worse than the worst examples I have seen
> in my experiments with parallelising interaction nets
> (
>    http://www.cas.mcmaster.ca/~kahl/Haskell/HINet/
>    http://eptcs.web.cse.unsw.edu.au/paper.cgi?DCM2014:8
> ),
> which makes me curious what is going on there.
>
> I also tried adding
>
>   -feager-blackholing
>
> to the ghc-options in a different install ---
> if actual parallelisation is happening,
> this should reduce duplication of computation,
> and is recommended for things that are intended to run in parallel.
> (I haven't seen speed-ups with that yet,
>   but I have seen a <<loop>> reported more precisely
>   in my interaction net experiments.)
> With Agda compiled with -feager-blackholing,
> while checking the standard library with -N1, I get:
>
>       Finished Data.Bool.Base.
>   50374120   8877328   9098816  0.03  0.03    0.75    1.08    0    0  (Gen:  1)
> agda: <<loop>>
>
>
> Now this makes me really curious what is going on there!
>
> (Some lack of laziness in the sharing implementation?)
>
> Since I have not been able to closely follow Agda development recently:
> What is the general context of current developments for these effects?
>
>
>
> Wolfram
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/