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

[Wolfram Kahl]

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