Re: [tlaplus] Re: Fairness in programming languages

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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