[Agda] Type-checker evaluator performance

[Liam O'Connor]

Alright,

I was able to type check the file in about 10 minutes on a newish Macbook Pro with 16GB of RAM — but it required basically all 16GB (about 15.5GB actually). Even a heap size of 14GB was too small.

At least I know it works!

Now I’m still interested in improving these numbers, but at least this stop my project in its tracks :)

--  
Liam 

On 2 February 2016 at 5:48:20 AM, Liam O'Connor (liamoc at cse.unsw.edu.au) wrote:
> Thanks for the detailed advice, Wolfram. Copied it into my org notes. If I limit the heap  
> size it should stop it getting OOM killed anyway.
>  
> 6GB doesn’t seem to be enough. I got heap exhausted after about 6 minutes. I’ll try a bigger  
> heap size on a beefier machine tomorrow.
>  
> I still think I’ve triggered a performance bug in Agda though. Before, this would run  
> for 5-10 minutes and check without hitting OOM, and now it’s taking at least 10 minutes,  
> usually longer, and running out of memory. Unfortunately I didn’t put the code in git  
> when I had a working version, so I don’t have access to the working, pre-cleanup code :/  
>  
> I’m beginning to suspect that I may not have ever tried to check this theorem after I introduced  
> the parameterised modules for the CTL logic and the GCL language. It’s possible that  
> doing this parameterisation has triggered the bug Andrea mentioned. I’ll try the patch  
> provided and see if that helps.
>  
> Worst case, I can remove those modules, but that would be an enormous pain, adding parameters  
> to every definition.
>  
> --
> Liam
>  
>  
> On 2 February 2016 at 5:28:42 AM, Wolfram Kahl (kahl at cas.mcmaster.ca) wrote:
> > Hi Liam,
> >
> > I am not addressing your real concern, but this may still
> > give you better chances of having your stuff type-checked in general:
> >
> > > I found that Agda would just get OOM killed before
> > > finishing, and it would take at least 10 minutes before getting
> > > OOM-killed, using all 8GB of my RAM and 4GB of my swap.
> >
> > I recommend to NEVER run Agda without specifying the heap,
> > e.g.:
> >
> > agda +RTS -M6G -H6G -A128M -S -RTS -i . -i $(agdalib) MyModule.lagda
> >
> > (Also run htop in another terminal to see what is going on.
> > http://hisham.hm/htop/
> > )
> >
> > -M6G Maximal heap.
> > With certain workloads, Agda will use any size of heap,
> > even though it might also succeed with smaller size.
> > And it does not know about your RAM and swap sizes...
> > So even though your run used all of your 12G of RAM+swap,
> > it may still succeed with -M6G. (But it also may not...)
> >
> > If you kill your firefox first, you may be able to go to 6.5G
> > or even 7G. If you work without desktop environment, and preferably also without X11,  
> > perhaps even 7.2G to 7.5G.
> > A stopped firefox can be pushed out into swap, but a live firefox will fight back.
> > (A swapped-out firefox takes ages to swap back in, so better kill it,
> > and restore session later.)
> > If you give Agda -M7.2G in your normal environment,
> > it will push out everything else (that does not fight back sufficiently) into swap,  
> > and if it succeeds, then run mostly happily.
> > But don't move your mouse nor expect reactions from your terminals and window managers.  
> > If you don't limit Agda's heap: Once Agda starts swapping its own pages,
> > you can forget it: Kill it.
> >
> > -H6G Start heap: If your Agda process is going to be big anyway, give it that start heap.  
> > You will see that it does not ask for all of it from the OS immediately,
> > but only when it finds a use for it.
> > For some small tasks (I believe including the standard library),
> > Agda never uses a large heap.
> > But if it does need a large heap, and you specified a smaller start heap
> > (e.g. by not passing -H), the GHC RTS will waste quite some time growing it
> > in small increments.
> >
> > -A128M Allocation area: Perhaps surprisingly, this makes my Agda runs much faster,  
> > by taking out the nervousness from the garbage collector.
> > On my 16G machines, I normally run +RTS -M10G -H10G -A1G -S -RTS.
> >
> > -S (only when running from the command line):
> > See how much heap is live after each garbage collection.
> > If you see it doing major (i.e., generation 1) garbage collections all the time,
> > just below the max heap size, it is spending fmost of its time garbage collecting,
> > and not getting any work done; then it is normally only going to be a question of time
> > (minutes to hours) until it runs out of heap, so you might just as well kill it,
> > and restart it with more heap if possible.
> > Another pattern I am seeing occasionally: It grows the live heap extremely slowly,  
> > doing only minor collections for hours. This tends to be deadly;
> > I have had it run for a week until it ran out of 50GB heap.
> >
> > I have recently only used Agda as 64-bit executable; I have modules that need 5G,
> > 6G, 8G, 9G, 10G, 11G, 13.5G. I have occasionally run Agda in heaps as large a 256G,
> > but so far have never seen anything typecheck that didn't also check with just 14G.
> >
> >
> > Hope this helps!
> >
> >
> > Wolfram
> >
>  
>