[Agda] Type-checker evaluator performance

Wed Feb 3 17:40:22 CET 2016

Yes, very clear, thank you!
Jacques
PS: perhaps such pieces of advice should go on to the wiki?

On 2016-02-03 11:23 , Ulf Norell wrote:
> Abstracting from the details of this particular example, the problem 
> is the following: You want to construct a proof of some proposition P 
> using some sort of search procedure that may or may not deliver an 
> actual proof. So you define
>
>   search : Maybe P
>
>   proof : P
>   proof = unMaybe search
>
> where
>
>   unMaybe : (m : Maybe A) {_ : IsJust m} -> A
>   unMaybe nothing {}
>   unMaybe (just x) _ = x
>
> When type checking 'proof' the type checker has to run 'search' to see 
> that it is indeed 'just' something so that the implicit IsJust proof 
> can be filled in. The important thing to note here is that 'search' 
> only needs to be evaluated far enough to discover that it is a 'just' 
> and no further. This means that we should make getting to the 'just' 
> constructor as cheap as possible.
>
> Consider what happens if you implement search in the most 
> straightforward way, simply running the search in the Maybe monad. In 
> this case you need to traverse the search space and build up the proof 
> object (which may be very large), at every step checking that all the 
> substeps came back 'just'. You don't get the final 'just' until you 
> have created the entire proof object.
>
> The alternative that I'm advocating is that you split the search 
> procedure into a test and a soundness proof for the test:
>
>   test : Bool
>   sound : T test -> P
>
> Here the soundness proof is responsible for constructing the proof 
> object, assuming that the test came back 'true'. We can then implement 
> the search as follows:
>
>   search : Maybe P
>   search with T? test
>   ... | yes p = just (sound p)
>   ... | no _ = nothing
>
> Now, in order to get to the 'just' constructor we only have to run 
> 'test' and we don't have to worry at all about constructing the proof 
> object.
>
> Concretely what I did in the me-em example was replace the 'ag' and 
> 'af' functions by two new functions 'ag-now' and 'af-now' implemented 
> as 'search' above (with tests 'ag-test' and 'af-test', and soundness 
> proofs 'ag-proof' and 'af-proof').
>
> I hope this clarifies things.
>
> / Ulf
>
>
>
> On Wed, Feb 3, 2016 at 3:34 PM, Jacques Carette <carette at mcmaster.ca 
> <mailto:carette at mcmaster.ca>> wrote:
>
>     Where can one read more about "no-eta-equality" ?  I believe that
>     some of my work could benefit from this as well.
>
>     Similarly, I sought to learn from the changes you did
>     https://github.com/UlfNorell/me-em/commit/5930ad6b155244a1ba85abc36a0e79c1333ca7f4
>     but while I can "read the code", I can't quite understand how this
>     matches your high-level description.  Could you comment a bit
>     about this?  I believe that this would be well worth it, and may
>     indeed help achieve a reduction in Agda-blame, as outlined in the
>     first paragraph.
>
>     Jacques
>
>
>     On 2016-02-03 04:31 , Ulf Norell 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
>>     <liamoc at cse.unsw.edu.au <mailto: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 <mailto:Agda at lists.chalmers.se>
>>         https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>
>>
>>     _______________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto: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/1ac68852/attachment-0001.html