On Lamport’s “Teaching Concurrency”

Uri Abraham, Distributed Computing & Education Column by Juraj Hromkovic, Stefan Schmid


In his article Teaching Concurrency Lamport stresses the importance of
invariants for the education of engineers and computer students, and presents
a short algorithm with a challenge to the reader: find an invariant with which
a certain simple property of that distributed algorithm can be proved. Our
aim is to compare the invariant proof approach to a dierent one which uses
Tarskian system executions rather than invariants. By comparing the details
of the two proofs for this simple algorithm we gain a better understanding
of these approaches.

Full Text:



  • There are currently no refbacks.