On Lamport’s “Teaching Concurrency”

Abstract

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.