[Agda] Type-checker evaluator performance

[Liam O'Connor]

Oh, I was not intending to blame Agda here for my performance problems. I welcome any improvements, either to Agda or my code. Clearly I lack the expertise to diagnose the performance problems accurately anyway.

Thanks for your patches! I hadn’t realised that I was doubling everything up by using the Maybe monad as I have. Thanks for pointing it out. I’ll work on a new version of the whole library that alleviates that issue. I’ll also merge your patches tomorrow.

Thanks again,

Liam


On 3 February 2016 at 8:31:58 PM, Ulf Norell (ulf.norell at gmail.com) wrote:
> I think it's unfortunate, if perhaps not completely undeserved, that Agda
> gets blamed every time a program is slow or uses a lot of memory. When
> people are writing slow Haskell programs their first thoughts are "maybe I
> should try to optimise my program", not "maybe someone should optimise GHC"
> and I wish we could have a little more of that for Agda programs. There are
> certainly performance problems in Agda's compile time evaluator
> (call-by-name, interpretation overhead, etc) but that doesn't mean that you
> can't write programs that perform reasonably well.
>  
> I had a look at your code and the main performance problem seems to be that
> you are too strict in the proof objects produced by the model checker. In
> your example the correctness proof of Peterson's algorithm consists of four
> (I think) complete state graphs (with ~14k states) decorated with proofs
> that you build up eagerly before deciding that you have a valid proof. If
> you instead separate the decision procedure from the construction of the
> proof object you only need to run the former to be sure that you have a
> proof, and can evaluate the latter lazily as you need it. I forked [1] your
> repo and tried this out. The Examples module checks in 26s and uses 900M
> memory on my machine. Another thing I tried is to use a pair type without
> eta equality for the models (in my experience eta equality and call-by-name
> is a major source of inefficiency). This saves you another 30% time and
> space.
>  
> / Ulf
>  
> [1] https://github.com/UlfNorell/me-em
>  
>  
> On Mon, Feb 1, 2016 at 9:46 AM, Liam O'Connor  
> wrote:
>  
> > Hi all,
> >
> > I’m currently using the development version of Agda, and I’ve been working
> > on using the evaluation in type checking to embed proof search procedures
> > inside Agda.
> >
> > https://github.com/liamoc/me-em
> >
> > Now, one of the applications of this technique is a model checker for a
> > fragment of CTL on the guarded command language (*).
> >
> > Here is an example, where I use the model checker to verify peterson’s
> > synchronisation algorithm.
> >
> > https://github.com/liamoc/me-em/blob/master/GCL/Examples.agda#L91
> >
> > Before I cleaned this code up and put it on GitHub, it was all in one
> > file. I can affirm that I was able to type check the code then. Today,
> > after splitting it into multiple files, and cleaning it up a little bit, 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.
> >
> > Going back to the original, single-file version, it now also fails to
> > finish checking and gets OOM-killed, so perhaps the multiple-files thing
> > isn’t causing the issue.
> >
> > (Perhaps I just used a bit of disk space and now it’s running out of swap).
> >
> > Anyway, I’ll try this on a machine with more memory (RAM and swap) later,
> > but is there any plan to improve performance (both in time and space) of
> > the type-checker evaluator? I appreciate that what I’m trying to do is not
> > something which it was designed to handle, but it _was working_ at some
> > point.
> >
> > BTW, it seems to make no difference whether I use sharing or not, but when
> > I got it to successfully check yesterday it was using sharing.
> >
> > (*) If you’ve seen the paper I wrote on this, note that the model checker
> > is substantially different now.
> >
> > (*) Also note that originally the definition for petersons-search read:
> >
> > petersons-search
> > = search $
> > and′ mutex? (and′ sf? termination?)
> > (model petersons initialState)
> >
> > but I gave it a fixed depth of 25 just to stop it doing any unnecessary
> > searching.
> >
> > Liam
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>