Role-Based Symmetry Reduction of Fault-tolerant Distributed Protocols with Language Support?

Abstract. Fault-tolerant (FT) distributed protocols (such as group mem-bership, consensus, etc.) represent fundamental building blocks for many practical systems, e.g., the Google File System. Not only does one desire rigor in the protocol design but especially in its verification given the complexity and fallibility of manual proofs. The application of model checking (MC) for protocol verification is attractive with its full au-tomation and rich property language. However, being an exhaustive ex-ploration method, its scalable use is very much constrained by the overall number of different system states. We observe that, although FT dis-tributed protocols usually display a very high degree of symmetry which stems from permuting different processes, MC efforts targeting their au-tomated verification often disregard this symmetry. Therefore, we pro-pose to leverage the framework of symmetry reduction and improve on existing applications of it by specifying so called role-based symmetries. Our secondary contribution is to define a high-level description language called FTDP to ease the symmetry aware specification of FT distributed protocols. FTDP supports synchronous as well as asynchronous proto-cols, a variety of fault types, and the specification of safety and liveness properties. Specifications written in FTDP can directly be analyzed by tools supporting symmetry reduction. We demonstrate the benefit of our approach using the example of well-known and complex distributed FT protocols, specifically Paxos and the Byzantine Generals.