Re: [tlaplus] Re: Fairness in programming languages

On Thursday, 11 November 2021 at 04:04:53 UTC-3 Leslie Lamport wrote:

You may want to use a sorting algorithm to sort millions of elements. I defy you to find a sorting algorithm that correctly sorts any 4 elements but incorrectly sorts a million elements--without writing something like "if N =< 4 then ...". The same applies to millions of processes. The problems that depend on scale are performance problems, not correctness problems. For particular performance problems, there are things one can try to do. For example, you can try to verify an upper bound on the number of messages taken to do something as a function of the number of processes. But as far as I know, that is generally done in industry by informal reasoning and testing, and it is not effective at finding rare problems.

Leslie
On Wednesday, November 10, 2021 at 2:45:20 PM UTC-8 jone...@xxxxxxxxx wrote:
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