[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Wed, 10 Nov 2021 23:04:53 -0800 (PST)*References*: <fb01eabf-d7ff-40a1-9187-10232a9231bdn@googlegroups.com> <4536a16f-dbdc-4b48-9f54-bfd8df795193n@googlegroups.com> <d61c9c8a-09ed-2875-e196-71270259f974@lemmster.de> <CABW84KzOsRK18Z_zxO9WReOYAOLvs4Hu9i8==b=iu7PJeLJ47w@mail.gmail.com> <8932e61d-4ac3-0de1-eb4d-a855ea96b36a@lemmster.de> <dd9722fc-314d-48b6-9b23-8eb6b7da4618n@googlegroups.com>

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?JonesOn 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

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/040ea8da-af5e-4b91-afc2-60fc78a8e8fen%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Re: Fairness in programming languages***From:*Jones Martins

**References**:**[tlaplus] Fairness in programming languages***From:*Jones Martins

**[tlaplus] Re: Fairness in programming languages***From:*Willy Schultz

**Re: [tlaplus] Re: Fairness in programming languages***From:*Markus Kuppe

**Re: [tlaplus] Re: Fairness in programming languages***From:*Jones Martins

**Re: [tlaplus] Re: Fairness in programming languages***From:*Markus Kuppe

**Re: [tlaplus] Re: Fairness in programming languages***From:*Jones Martins

- Prev by Date:
**Re: [tlaplus] Re: Fairness in programming languages** - Next by Date:
**Re: [tlaplus] Re: Fairness in programming languages** - Previous by thread:
**Re: [tlaplus] Re: Fairness in programming languages** - Next by thread:
**Re: [tlaplus] Re: Fairness in programming languages** - Index(es):