Abstract
We derive a \(3f\!+\!1\) process Byzantine Paxos consensus algorithm by Byzantizing a variant of the ordinary Paxos algorithm—that is, by having \(2f\!+\!1\) nonfaulty processes emulate the ordinary Paxos algorithm despite the presence of f malicious processes. We have written a formal, machine-checked proof that the Byzantized algorithm implements the ordinary Paxos consensus algorithm under a suitable refinement mapping.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)
Castro, M., Liskov, B.: Practical byzantine fault tolerance and proactive recovery. ACM Transactions on Computer Systems 20(4), 398–461 (2002)
Fischer, M.J., Lynch, N., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. Journal of the ACM 32(2), 374–382 (1985)
Guerraoui, R., Vukolić, M.: Refined quorum systems. Distributed Computing 23(1), 1–42 (2010)
Lamport, L.: Mechanically checked safety proof of a byzantine paxos algorithm, http://research.microsoft.com/users/lamport/tla/byzpaxos.html . The page can also be found by searching the Web for the 23-letter string obtained by removing the “-” from, uid-lamportbyzpaxosproof
Lamport, L.: The part-time parliament. ACM Transactions on Computer Systems 16(2), 133–169 (1998)
Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2003)
Lamport, L.: Fast paxos. Distributed Computing 19(2), 79–103 (2006)
Lamport, L.: The pluscal algorithm language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 36–60. Springer, Heidelberg (2009)
Lamport, L., Malkhi, D., Zhou, L.: Vertical paxos and primary-backup replication. In: Tirthapura, S., Alvisi, L. (eds.) Proceedings of the 28th Annual ACM Symposium on Principles of Distributed Computing, PODC 2009, pp. 312–313. ACM, New York (2009)
Lamport, L.B.: Fast byzantine paxos. United States Patent 7620680, filed (August 15, 2002) issued (November 17, 2009)
Lamport, L.B., Massa, M.T.: Cheap Paxos. United States Patent 7249280, filed (June 18, 2004) issued (July 24, 2007)
Lampson, B.W.: The ABCDs of Paxos, http://research.microsoft.com/lampson/65-ABCDPaxos/Abstract.html
Martin, J.-P., Alvisi, L.: Fast byzantine consensus. In: Proceedings of the International Conference on Dependable Systems and Networks (DSN 2005), Yokohama, pp. 402–411. IEEE Computer Society, Los Alamitos (2006)
Oki, B.M.: Viewstamped replication for highly available distributed systems. Technical Report MIT/LCS/TR-423, MIT Laboratory for Computer Science (Ph.D. Thesis) (August 1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lamport, L. (2011). Byzantizing Paxos by Refinement. In: Peleg, D. (eds) Distributed Computing. DISC 2011. Lecture Notes in Computer Science, vol 6950. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24100-0_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-24100-0_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24099-7
Online ISBN: 978-3-642-24100-0
eBook Packages: Computer ScienceComputer Science (R0)