Skip to main content
SpringerLink
Log in

Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol

  • Conference paper
  • First Online:
Formal Methods – The Next 30 Years (FM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

Included in the following conference series:

  • 1398 Accesses

Abstract

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).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In our Event-B model, we actually use a pure first-order axiomatization, presented e.g. in [15], which allows SMT solvers to deal with many proofs automatically.

  2. 2.

    Not to be confused with Chord’s finger tables whose purpose is to support efficient query routing [17, Sect. 4.3].

  3. 3.

    An event with guard and body will give rise to an Event-B event with guard and body , and to Event-B events (resp ) with guard and body (resp. with guard and body .

  4. 4.

    We write (resp. ) for list concatenation (resp. cons), and (resp. ) for \(\texttt {x := x} \setminus \texttt {s}\) (resp. \(\texttt {x := x} \cup \texttt {s}\)). Abusing notation, a singleton set \(\{ \texttt {s} \}\) is written \(\texttt {s}\).

  5. 5.

    Given an event e, [e](p) is the weakest precondition ensuring that e terminates in a state satisfying p.

  6. 6.

    Since all the first successors are alive in the ideal state, \(\texttt {bestSucc}\) always points to the first successor.

  7. 7.

    \(\text {\texttt {dom}}\) denotes the domain of a relation or a function.

  8. 8.

    The Chord Property 3 about the \(\texttt {Stabilizing}\) function is preserved by \(\text {\texttt {fail}}\) and thus does not impact operating assumptions.

  9. 9.

    Once a macro-state is reached, the system cannot leave it.

  10. 10.

    \(\text {\texttt {ran}} \) denotes the range of a relation or a function.

  11. 11.

    Technically, we have an Event-B model for each phase defined as a refinement of the Event-B machine modelling the Chord protocol, where the MS of the preceding phase is stated as an invariant of the current phase.

  12. 12.

    In Event-B, this structured variant is encoded as a single set using the Cartesian product and union.

References

  1. Abrial, J.R.: Modeling in Event-B. Cambridge University Press, Cambridge (2009). https://doi.org/10.1017/cbo9781139195881

    Book  Google Scholar 

  2. Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010). https://doi.org/10.1007/s10009-010-0145-y

    Article  Google Scholar 

  3. Bakhshi, R., Gurov, D.: Verification of peer-to-peer algorithms: a case study. Electron. Notes Theor. Comput. Sci. 181, 35–47 (2007). https://doi.org/10.1016/j.entcs.2007.01.052

    Article  Google Scholar 

  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

  5. Brunel, J., Chemouil, D., Tawa, J.: Analyzing the fundamental liveness property of the Chord protocol. In: Formal Methods in Computer-Aided Design, Austin, USA, October 2018. https://doi.org/10.23919/fmcad.2018.8603001. https://hal.archives-ouvertes.fr/hal-01862755

  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 

  9. Li, X., Misra, J., Plaxton, C.G.: Active and concurrent topology maintenance. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol. 3274, pp. 320–334. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30186-8_23

    Chapter  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

  14. Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. PACMPL 2(POPL), 26:1–26:33 (2018). https://doi.org/10.1145/3158114

    Article  Google Scholar 

  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

  17. Stoica, I., Morris, R., Karger, D., Kaashoek, M.F., Balakrishnan, H.: Chord: a scalable peer-to-peer lookup service for internet applications. ACM SIGCOMM Comput. Commun. Rev. 31(4), 149–160 (2001). https://doi.org/10.1145/964723.383071

    Article  Google Scholar 

  18. Stoica, I., et al.: Chord: a scalable peer-to-peer lookup protocol for Internet applications. IEEE/ACM Trans. Netw. (TON) 11(1), 17–32 (2003). https://doi.org/10.1109/tnet.2002.808407

    Article  Google Scholar 

  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 

  21. Zave, P.: Using lightweight modeling to understand Chord. ACM SIGCOMM Comput. Commun. Rev. 42(2), 49–57 (2012). https://doi.org/10.1145/2185376.2185383

    Article  Google Scholar 

  22. Zave, P.: A practical comparison of Alloy and Spin. Formal Aspects Comput. 27(2), 239 (2015). https://doi.org/10.1007/s00165-014-0302-2

    Article  Google Scholar 

  23. Zave, P.: Reasoning about identifier spaces: how to make Chord correct. IEEE Trans. Softw. Eng. 43(12), 1144–1156 (2017). https://doi.org/10.1109/TSE.2017.2655056

    Article  Google Scholar 

Download references

Acknowledgements

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).

Author information

Authors and Affiliations

  1. IRIT CNRS UPS, Université de Toulouse, Toulouse, France

    Jean-Paul Bodeveix & Mamoun Filali

  2. ONERA DTIS, Université de Toulouse, Toulouse, France

    Julien Brunel & David Chemouil

Authors
  1. Jean-Paul Bodeveix
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Julien Brunel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Chemouil
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mamoun Filali
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David Chemouil .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bodeveix, JP., Brunel, J., Chemouil, D., Filali, M. (2019). Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation