On the Automated Implementation of Time-Based Paxos Using the IOA Compiler

Paxos is a well known algorithm for achieving consensus in distributed environments with uncertain processing and communication timing. Implementations of its variants have been successfully used in the industry (eg., Chubby by Google, Autopilot cluster management in Bing by Microsoft, and many others). This paper addresses the challenge of the manual coding of complex distributed algorithms, such as Paxos, where this is an error prone process. Our approach in ensuring correct implementation is to use a verified automated translator to compile a source specification that has been proven to be itself correct. We use specification of the Paxos algorithm in the General Timed Automata (GTA) model, an extension of I/O Automata, as input to an augmented compiler for the Input/Output Automata notation (a.k.a., the IOA compiler) in order to generate executable Java code. The resulting code is interfaced with MPI for communication needs. We have extended the IOA compiler to support a version o...

• Type: Journal
• Year: 2010
• Where: OPODIS
• Authors: Chryssis Georgiou, Procopis Hadjiprocopiou, Peter M. Musial
• Keywords: Algorithm, Distributed And Parallel Computing, IOA Compiler, OPODIS 2010, Paxos