[Agda] Type-checker evaluator performance

[Liam O'Connor]

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