GNATprove already uses quite a few techniques to avoid doing the same work over and over again. This older blog post explains the main mechanisms that are in play. In this blog post, we describe yet another mechanism, that can decrease the work done by gnatprove considerably. In this other post we have described how we changed the architecture of the SPARK tools to achieve more parallelism.

When GNATprove analyses your SPARK program, it internally creates an intermediate file in the Why3 format, and then spawns a program called "gnatwhy3" to process this file. It is usually in the gnatwhy3 process that GNATprove spends most of its analysis time. Couldn't we save a lot of this time if we "cache" calls to gnatwhy3? That is, we could detect if the intermediate Why3 file is the same as the last time, and no other relevant conditions have changed, and simply take the analysis results of last time.

This is exactly what this new SPARK feature does. It computes a hash of the intermediate file and all relevant parameters, and uses a memcached server to check if a previous run of gnatwhy3 exists with this hash. If yes, the result of the last analysis is retrieved from the server. If not, the gnatwhy3 tool is run as usual.

The nice property of this new feature is that the memcached server can be shared across members of a team. All you need is to set up a machine on your network which has such a server running. Memcached is free, open source and very easy to set up. Then you can specify this server to your invocation of GNATprove if you add ``--memcached-server=hostname:portnumber``  to the commmand line. If your team uses this option, and your colleague developer has just run the SPARK tools on a checkout of your project, you should see speedups in your own usage of the tools (and vice-versa).