García-Pérez, Á;
Gotsman, A;
Meshman, Y;
Sergey, I;
(2018)
Paxos Consensus, Deconstructed and Abstracted.
In: Ahmed, A, (ed.)
Programming Languages and Systems.
(pp. pp. 912-939).
Springer: Cham, Switzerland.
Preview |
Text
Sergey_2018_Book_ProgrammingLanguagesAndSystems_extracted.pdf - Published Version Download (1MB) | Preview |
Abstract
Lamport’s Paxos algorithm is a classic consensus protocol for state machine replication in environments that admit crash failures. Many versions of Paxos exploit the protocol’s intrinsic properties for the sake of gaining better run-time performance, thus widening the gap between the original description of the algorithm, which was proven correct, and its real-world implementations. In this work, we address the challenge of specifying and verifying complex Paxos-based systems by (a) devising composable specifications for implementations of Paxos’s single-decree version, and (b) engineering disciplines to reason about protocol-aware, semantics-preserving optimisations to single-decree Paxos. In a nutshell, our approach elaborates on the deconstruction of single-decree Paxos by Boichat et al. We provide novel non-deterministic specifications for each module in the deconstruction and prove that the implementations refine the corresponding specifications, such that the proofs of the modules that remain unchanged can be reused across different implementations. We further reuse this result and show how to obtain a verified implementation of Multi-Paxos from a verified implementation of single-decree Paxos, by a series of novel protocol-aware transformations of the network semantics, which we prove to be behaviour-preserving.
| Type: | Proceedings paper |
|---|---|
| Title: | Paxos Consensus, Deconstructed and Abstracted |
| Event: | 27th European Symposium on Programming (ESOP 2018) |
| ISBN-13: | 978-3-319-89883-4 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-319-89884-1_32 |
| Publisher version: | https://doi.org/10.1007/978-3-319-89884-1_32 |
| Language: | English |
| Additional information: | Copyright © The Author(s) 2018. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10046850 |
Archive Staff Only
 |
View Item |
