Sciweavers

Share
OPODIS
2010

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

8 years 11 months ago
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...
Chryssis Georgiou, Procopis Hadjiprocopiou, Peter
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where OPODIS
Authors Chryssis Georgiou, Procopis Hadjiprocopiou, Peter M. Musial
Comments (0)
books