Nowadays, most machines are multi-core machines, and it would be silly to use just one core. That's why many tools, such as make or gnatmake have a command line argument "-j<n>" which will allow it to use up to n cores. The SPARK 2014 command-line tool gnatprove is no exception. It has to run many instances of the prover to discharge each and every check in a SPARK program, so it makes perfect sense to run those in parallel.

Behind the scenes, gnatprove uses the Why3 tool, which already supports parallelism. But the problem is that gnatprove doesn't only run a single Why3 process, but one for each unit, and there can be hundreds of units in a SPARK program. So how to do parallelism properly?

The simple solution is to run n Why3 processes in parallel, where each of them runs up to n proof processes in parallel. But this clearly allows much too many processes, namely up to n * n processes to be run in parallel, which will make the machine unusable. In fact, if we don't want to change the architecture of the tool, and if we want to be sure to not exceed n proof processes at any given time, we are only allowed to run k Why3 processes at once, each of them allowed to run l proof processes, such that k * l = n. There are three simple solutions to this equation:

• k = 1 and l = n, that is, run each of the Why3 processes sequentially, and each of them is allowed to run n proof processes.
• k = n and l = 1, that is run n Why3 processes in parallel, but each of them runs the proof processes sequentially.
• k = l = sqrt(n). This is kind of a mix of both, which allows for some  Why3 processes in parallel, each of them can spawn some proof  processes.

The first two are clearly not optimal, because in both solutions, a single long-running VC can block the entire process. The third one is also not very good. The problem is that the square root grows very slowly, so even when allowing 24 processes, you can only run 4 Why3 processes. The conclusion is that we need indeed to change the architecture of the tool.

They say that there is no problem in computing that you can't solve with an extra layer of indirection, and that's exactly what we did in this case. Instead of Why3 running the proof processes itself, it delegates this task to a "proof server". This proof server is allowed to run up to n proof processes. Now we can safely run n Why3 processes in parallel. Each of them will send it's proof requests to the server, which runs the proof and reports back the result. At any given time, only n proof processes are running.

On one of our larger tests, we could reduce the running time of gnatprove from 3 minutes to less than a minute, while allowing the same number of parallel proof processes.

Note that this feature is not SPARK 2014 release of this week. It will be in the release scheduled for 2015.