[Agda] Type-checker evaluator performance

[Liam O'Connor]

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
>