Wow, that is one large proof.
Am I right in assuming that, depending on the scale of the algorithm (I'm thinking “planetary scale”), it's important to prove instead of only model check an algorithm? Model checking, say, Paxos with thousands of processes, even with dozens of workers, will take months to finish. Putting some effort into proving the algorithm, thus, is critical to ensure correctness of large-scale implementations?
Jones
On Wednesday, 10 November 2021 at 19:28:10 UTC-3 Markus Alexander Kuppe wrote:
On 11/10/21 2:00 PM, Jones Martins wrote:
> May I ask in your BlockingQueue spec, why do you need to prove Deadlock
> freedom in the sense that why is it necessary? Is it good practice to
> prove specs of its size?
In the BlockingQueue spec, the prove serves mainly as an illustration of
TLAPS. However, it still proves that the algorithm is deadlock-free for
*any positive number* of processes. In contrast, model-checking only
proves that the algorithm works for a particular, finite number of
processes.
TLA+ specs are usually small (up to ~2k LOC), yet it is still worth
writing a proof for some of them (think Paxos). Also, contrast, e.g.,
the size of the spec and the proof [2] of a non-blocking algorithm for
process renaming [1].
Markus
[1] http://pardi.enseeiht.fr/Papers/TAP2019.pdf
[2] http://hurault.perso.enseeiht.fr/RenamingProof/Renaming.tla