Modeling Consensus in a Process Calculus
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.