Proof of distributed algorithms: an exercise
K. Mani Chandy, Jayadev Misra · Addison-Wesley Longman Publishing Co., Inc. eBooks · 1991
It is generally assumed that formal proofs of programs are considerably longer and more tedious than their informal counterparts. Informal proofs employ a form of common sense reasoning whereby “obvious” facts are often omitted and the proof steps rely upon the intuition of the reader. Typically informal proofs are operational; arguments consist of the properties of program executions as they unfold over time. Our goal in this paper is to suggest, by means of an example, that formal proofs can be made as concise as the informal ones. This argument rests upon two observations: (1) informal proofs tend to be long and difficult (in addition to being error-prone) when there are many interleaved execution sequences to consider, as is the case in multiprocess programs, and (2) formal proofs can be made concise by employing a logic that is appropriate for the problem domain and whose operators possess a number of useful properties that can be exploited in proofs. In recent years, we have developed a programming and proof theory, called UNITY, Chandy and Misra [1988]. Our experience in using the UNITY proof theory on a wide range of problems has led us to believe that formal proofs need not be outrageously long or tedious. In this paper, we apply the UNITY proof theory to a problem in distributed computing—termination detection. We specify the problem and develop a correctness proof of a solution without relying upon the operational aspects of program execution. Use of our logic allows us to eliminate arguments about a program’s execution sequences. We believe strongly that formal proofs cannot be made concise as long as they mimic the arguments in the informal proofs. Most of this paper is about UNITY theory and specification of message communicating processes; only sections 4 and 6 contain the proof of the termination detection algorithm. The paper is selfcontained: no familiarity with UNITY or termination detection is assumed.