{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T02:35:37Z","timestamp":1784342137572,"version":"3.55.0"},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2012,3,29]],"date-time":"2012-03-29T00:00:00Z","timestamp":1332979200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGCOMM Comput. Commun. Rev."],"published-print":{"date-parts":[[2012,3,29]]},"abstract":"<jats:p>Correctness of the Chord ring-maintenance protocol would mean that the protocol can eventually repair all disruptions in the ring structure, given ample time and no further disruptions while it is working. In other words, it is \"eventual reachability.\" Under the same assumptions about failure behavior as made in the Chord papers, no published version of Chord is correct. This result is based on modeling the protocol in Alloy and analyzing it with the Alloy Analyzer. By combining the right selection of pseudocode and textual hints from several papers, and fixing flaws revealed by analysis, it is possible to get a version that may be correct. The paper also discusses the significance of these results, describes briefly how Alloy is used to model and reason about Chord, and compares Alloy analysis to model-checking.<\/jats:p>","DOI":"10.1145\/2185376.2185383","type":"journal-article","created":{"date-parts":[[2012,4,17]],"date-time":"2012-04-17T12:53:13Z","timestamp":1334667193000},"page":"49-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":79,"title":["Using lightweight modeling to understand chord"],"prefix":"10.1145","volume":"42","author":[{"given":"Pamela","family":"Zave","sequence":"first","affiliation":[{"name":"AT&amp;T Laboratories -- Research, Florham Park, New Jersey, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,3,29]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"55","volume-title":"Proceedings of the 2nd Conference on Real, Large, Distributed Systems","author":"Freedman M. J.","year":"2005","unstructured":"M. J. Freedman , K. Lakshminarayanan , S. Rhea , and I. Stoica . Non-transitive connectivity and DHTs . In Proceedings of the 2nd Conference on Real, Large, Distributed Systems , pages 55 -- 60 . USENIX, 2005 . M. J. Freedman, K. Lakshminarayanan, S. Rhea, and I. Stoica. Non-transitive connectivity and DHTs. In Proceedings of the 2nd Conference on Real, Large, Distributed Systems, pages 55--60. USENIX, 2005."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043559"},{"key":"e_1_2_1_3_1","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann G. J.","year":"2004","unstructured":"G. J. Holzmann . The Spin Model Checker: Primer and Reference Manual . Addison-Wesley , 2004 . G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2004."},{"key":"e_1_2_1_4_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson D.","year":"2006","unstructured":"D. Jackson . Software Abstractions: Logic, Language, and Analysis . MIT Press , 2006 . D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006."},{"key":"e_1_2_1_5_1","first-page":"243","volume-title":"Proceedings of the 4th USENIX Symposium on Networked System Design and Implementation","author":"Killian C.","year":"2007","unstructured":"C. Killian , J. A. Anderson , R. Jhala , and A. Vahdat . Life, death, and the critical transition: Finding liveness bugs in systems code . In Proceedings of the 4th USENIX Symposium on Networked System Design and Implementation , pages 243 -- 256 , 2007 . C. Killian, J. A. Anderson, R. Jhala, and A. Vahdat. Life, death, and the critical transition: Finding liveness bugs in systems code. In Proceedings of the 4th USENIX Symposium on Networked System Design and Implementation, pages 243--256, 2007."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11558989_9"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/571825.571863"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095818"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/383059.383071"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2002.808407"},{"key":"e_1_2_1_12_1","volume-title":"EPFL NSL-REPORT-2009-007","author":"Yabandeh M.","year":"2009","unstructured":"M. Yabandeh , A. Anand , M. Canini , and D. Kosti . Almost-invariants: From bugs in distributed systems to invariants. Technical report , EPFL NSL-REPORT-2009-007 , 2009 . M. Yabandeh, A. Anand, M. Canini, and D. Kosti . Almost-invariants: From bugs in distributed systems to invariants. Technical report, EPFL NSL-REPORT-2009-007, 2009."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation. USENIX","author":"Yabandeh M.","year":"2009","unstructured":"M. Yabandeh , N. Knezevi , D. Kosti , and V. Kuncak . CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems . In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation. USENIX , April 2009 . M. Yabandeh, N. Knezevi , D. Kosti , and V. Kuncak. CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation. USENIX, April 2009."},{"key":"e_1_2_1_14_1","volume-title":"AT&T Laboratories|Research","author":"Zave P.","year":"2010","unstructured":"P. Zave . Lightweight modeling of network protocols: The case of Chord. Technical report , AT&T Laboratories|Research , January 2010 . P. Zave. Lightweight modeling of network protocols: The case of Chord. Technical report, AT&T Laboratories|Research, January 2010."},{"key":"e_1_2_1_15_1","volume-title":"1st International Workshop on Rigorous Protocol Engineering","author":"Zave P.","year":"2011","unstructured":"P. Zave . Experiences with protocol description. Technical report, AT&T Laboratories|Research, June 2011 . Presented at the 1st International Workshop on Rigorous Protocol Engineering , October 2011 , Vancouver, British Columbia. P. Zave. Experiences with protocol description. Technical report, AT&T Laboratories|Research, June 2011. Presented at the 1st International Workshop on Rigorous Protocol Engineering, October 2011, Vancouver, British Columbia."}],"container-title":["ACM SIGCOMM Computer Communication Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2185376.2185383","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2185376.2185383","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:01Z","timestamp":1750241161000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2185376.2185383"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,29]]},"references-count":14,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,3,29]]}},"alternative-id":["10.1145\/2185376.2185383"],"URL":"https:\/\/doi.org\/10.1145\/2185376.2185383","relation":{},"ISSN":["0146-4833"],"issn-type":[{"value":"0146-4833","type":"print"}],"subject":[],"published":{"date-parts":[[2012,3,29]]},"assertion":[{"value":"2012-03-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}