[Agda] Type-checker evaluator performance

[Liam O'Connor]

Thanks for the responses everyone.

@Andrea,

I definitely introduced parameterised modules, but I’m not sure if I did so before or after I last successfully checked the slow theorem. Nevertheless, do you think it’s advisable that I try your patch and see if it improves performance?

I know which line is slow, it’s this one https://github.com/liamoc/me-em/blob/master/GCL/Examples.agda#L97 which triggers the exhaustive search algorithm described above it. This is a large tree and I wouldn’t expect it to be instant or cheap, but I’d like it to be at least possible. 

@Peter

Ah, I was under the impression that ——sharing was supposed to fix this. I might see if there is some low-hanging rewriting I can do to my code to speed this up.

Regards,
Liam 


On 1 February 2016 at 9:32:32 PM, Peter Selinger (selinger at mathstat.dal.ca) wrote:
> Also, Agda uses a normal order evaluator that is not lazy. For
> example, any function that returns a pair will be evaluated twice. If
> you use such a function recursively, the evaluation time will be
> exponential. Also, if you write something like "let x = f y in (x , x)",
> f will be evaluated twice. It's often very tricky to rewrite your
> programs to avoid this effect, and even more tricky to prove
> properties about them afterwards. In my experience, turning on
> --sharing does not change this behavior. But maybe efforts are under
> way to fix this?
>  
> -- Peter
>  
> Andrea Vezzosi wrote:
> >
> > Did you introduce parametrized modules during the cleaning-up?
> >
> > If so you might have introduced problems similar to this issue:
> >
> > https://github.com/agda/agda/issues/1625
> >
> > Also, if you turn on interactive highlighting you'll get to see
> > approximately on which expression time is being spent during
> > typechecking.
> >
> > Best,
> > Andrea
> >
> >
> >
> > 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
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>  
>