Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Chord is a protocol providing a scalable distributed hash table over an underlying peer-to-peer network. It is very popular due to its simplicity, performance and claimed correctness. However, the original version of the Chord maintenance protocol, presented with an informal proof of correctness, was since then shown to be in fact incorrect. It is actually tricky to come up with a provably-correct version as the protocol combines data structures, asynchronous communication, concurrency, and fault tolerance. Additionally, the correctness property amounts to a form of stabilization, a particular kind of liveness property. Previous work only addressed automated proofs of safety; and pen-and-paper, or automated but much bounded, proofs of stabilization. In this article, we report on the first mechanized proof of the liveness property for Chord. Furthermore, our proof addresses the full parameterized version of the protocol, weakens previously-devised invariants and operating assumptions, and is essentially automated (requiring limited effort when manual assistance is needed).
KeywordsChord Distributed protocol Parameterized verification Liveness Stabilization proof
We warmly thank Pamela Zave for insightful discussions on the protocol and for her thorough reading of this article.
J. Brunel and D. Chemouil were partly financed by the European Regional Development Fund (ERDF) through the Operational Programme for Competitiveness and Internationalisation (COMPETE2020) and by National Funds through the Portuguese funding agency, Fundação para a Ciência e a Tecnologia (FCT) within project POCI-01-0145-FEDER-016826; and within the French Research Agency project FORMEDICIS (ANR-16-CE25-0007).
- 4.Bodeveix, J.P., Brunel, J., Chemouil, D., Filali, M.: A model in Event-B of the Chord protocol, July 2019. https://doi.org/10.5281/zenodo.3271455
- 6.Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), ACM –Association for Computing Machinery, October 2015. https://doi.org/10.1145/2815400.2815428
- 7.Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)Google Scholar
- 8.Lamport, L.: Specifying Systems: The TLA\(^+\) Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)Google Scholar
- 10.Liben-Nowell, D., Balakrishnan, H., Karger, D.: Analysis of the evolution of peer-to-peer systems. In: Proceedings of the Twenty-First Annual Symposium on Principles of Distributed Computing, pp. 233–242. ACM (2002). https://doi.org/10.1145/571860.571863
- 11.Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: Foundations of Software Engineering (2016). https://doi.org/10.1145/2950290.2950318
- 12.Marinković, B., Glavan, P., Ognjanović, Z.: Proving properties of the Chord protocol using the ASM formalism. Theor. Comput. Sci. 756, 64 – 93 (2019). https://doi.org/10.1016/j.tcs.2018.10.025, http://www.sciencedirect.com/science/article/pii/S0304397518306467
- 13.Merz, S., Lu, T., Weidenbach, C.: Towards verification of the pastry protocol using TLA\(^+\). In: 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, vol. 6722 (2011). https://doi.org/10.1007/978-3-642-21461-5_16
- 15.Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13–17 June 2016, pp. 614–630 (2016). https://doi.org/10.1145/2908080.2908118
- 16.Risson, J., Robinson, K., Moors, T.: Fault tolerant active rings for structured peer-to-peer overlays. In: 2005 The IEEE Conference on Local Computer Networks, 30th Anniversary, pp. 18–25. IEEE (2005). https://doi.org/10.1109/lcn.2005.69
- 19.Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 357–368 (2015). https://doi.org/10.1145/2737924.2737958
- 20.Zave, P.: Why the Chord ring-maintenance protocol is not correct. Technical report, AT&T Research (2011)Google Scholar