23-25 June 2010
(Joint work with Bernadette Charron-Bost, LIX, CNRS, Palaiseau, France)
Distributed algorithms are often quite subtle, in the way they operate and in the assumptions they make. Formal verification is therefore crucial in distributed computing. To facilitate their design and understanding, many existing distributed algorithms are structured in rounds: each process first sends messages, then receives messages from other processes, and finally makes a local state transition. However, existing formal models of distributed algorithms do not take advantage of this structure, but are based on a fine-grained description of systems whose individual processes are represented by communicating state machines.
Reduction theorems for concurrent and distributed algorithm have been studied since Lipton's seminal paper in 1975. Broadly speaking, they aim at pretending that certain sequences of events happen indivisibly, thus allowing verification to be carried out over coarser-grained models of algorithms and systems. We revisit this line of research and contribute a reduction theorem for distributed algorithms that are organized in communication-closed rounds, demonstrating its benefits on the verification of several consensus algorithms using model checking and theorem proving.