Derivation of a Simple Synchronization Algorithm - Lamport, Leslie (1987)
Chuck Thacker posed a little synchronization problem to me, which I solved with Jim Saxe's help. At that time, deriving concurrent algorithms was the fashion–the idea that you discover the algorithm by some form of black magic and then verify it was considered passé. So, I decided to see if I could have derived the algorithm from approved general principles. I discovered that I could–at least, informally–and that this informal derivation seemed to capture the thought process that led me to the solution in the first place.