[Agda] Type-checker evaluator performance

[Ulf Norell]

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 <liamoc at cse.unsw.edu.au>
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160203/5ca9ed11/attachment.html