Modeling Consensus in a Process Calculus

Uwe Nestmann

Consensus is known as one of the most important problems in the field of Distributed Algorithms, according to which a fixed number of communicating processes that initially have different opinions (values) must after some finite amount of time agree on one of these opinions. Many folklore results are known about the conditions under which there exist algorithms to solve Consensus. For example, it is impossible to solve Consensus in completely asynchronous systems, if even only one of the processes may crash. However, it is also known that solutions exist under the assumption of partial synchrony or the availability of certain unreliable failure detectors. Often, distributed algorithms are expressed in terms of pseudo-code and the relevant proofs are given in terms of natural language. In this talk, I report on ongoing work, where we study one of the well-known solutions (using a failure detector called Diamond-S) by formulating the respective algorithm as a term in some simple extended process calculus, while the proof is then exploiting the calculus' formal operational semantics.