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

Re: [tlaplus] Re: Fairness in programming languages

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].


[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/8932e61d-4ac3-0de1-eb4d-a855ea96b36a%40lemmster.de.