{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:26:55Z","timestamp":1777890415378,"version":"3.51.4"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031300431","type":"print"},{"value":"9783031300448","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T00:00:00Z","timestamp":1681689600000},"content-version":"vor","delay-in-days":106,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Distributed algorithms solving agreement problems like consensus or state machine replication are essential components of modern fault-tolerant distributed services. They are also notoriously hard to understand and reason about. Their complexity stems from the different assumptions on the environment they operate with, i.e., process or network link failures, Byzantine failures etc. In this paper, we propose a novel abstract representation of the dynamics of such protocols which focuses on quorums of responses (votes) to a request (proposal) that form during a run of the protocol. We show that focusing on such quorums, a run of a protocol can be viewed as working over a tree structure where different branches represent different possible outcomes of the protocol, the goal being to stabilize on the choice of a fixed branch. This abstraction resembles the description of recent protocols used in Blockchain infrastructures, e.g., the protocol supporting Bitcoin or Hotstuff. We show that this abstraction supports reasoning about the safety of various algorithms, e.g., Paxos, PBFT, Raft, and HotStuff, in a uniform way. In general, it provides a novel induction based argument for proving that such protocols are safe.<\/jats:p>","DOI":"10.1007\/978-3-031-30044-8_13","type":"book-chapter","created":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T20:28:25Z","timestamp":1681676905000},"page":"337-362","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Quorum Tree Abstractions of Consensus Protocols"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4261-090X","authenticated-orcid":false,"given":"Berk","family":"Cirisci","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2727-8865","authenticated-orcid":false,"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0734-7969","authenticated-orcid":false,"given":"Suha Orhun","family":"Mutluergil","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Aublin, P., Guerraoui, R., Knezevic, N., Qu\u00e9ma, V., Vukolic, M.: The next 700 BFT protocols. ACM Trans. Comput. Syst. 32(4), 12:1\u201312:45 (2015). https:\/\/doi.org\/10.1145\/2658994","DOI":"10.1145\/2658994"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Ben-Or, M.: Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract). In: Probert, R.L., Lynch, N.A., Santoro, N. (eds.) Proceedings of the Second Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 17-19, 1983. pp. 27\u201330. ACM (1983). https:\/\/doi.org\/10.1145\/800221.806707","DOI":"10.1145\/800221.806707"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Boichat, R., Dutta, P., Fr\u00f8lund, S., Guerraoui, R.: Deconstructing paxos. SIGACT News 34(1), 47\u201367 (2003). https:\/\/doi.org\/10.1145\/637437.637447","DOI":"10.1145\/637437.637447"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Bravo, M., Chockler, G.V., Gotsman, A.: Making byzantine consensus live. In: Attiya, H. (ed.) 34th International Symposium on Distributed Computing, DISC 2020, October 12-16, 2020, Virtual Conference. LIPIcs, vol.\u00a0179, pp. 23:1\u201323:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.DISC.2020.23","DOI":"10.4230\/LIPIcs.DISC.2020.23"},{"key":"13_CR5","unstructured":"Castro, M., Liskov, B.: Practical byzantine fault tolerance. In: Seltzer, M.I., Leach, P.J. (eds.) Proceedings of the Third USENIX Symposium on Operating Systems Design and Implementation (OSDI), New Orleans, Louisiana, USA, February 22-25, 1999. pp. 173\u2013186. USENIX Association (1999), https:\/\/dl.acm.org\/citation.cfm?id=296824"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Chand, S., Liu, Y.A., Stoller, S.D.: Formal verification of multi-paxos for distributed consensus. In: Fitzgerald, J.S., Heitmeyer, C.L., Gnesi, S., Philippou, A. (eds.) FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09995, pp. 119\u2013136 (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_8","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225\u2013267 (1996). https:\/\/doi.org\/10.1145\/226643.226647","DOI":"10.1145\/226643.226647"},{"key":"13_CR8","unstructured":"Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in the heard-of model. Int. J. Softw. Informatics 3(2-3), 273\u2013303 (2009), http:\/\/www.ijsi.org\/ch\/reader\/view_abstract.aspx?file_no=273 &flag=1"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Cirisci, B., Enea, C., Mutluergil, S.O.: Quorum tree abstractions of consensus protocols (2023). https:\/\/doi.org\/10.48550\/ARXIV.2301.09946, https:\/\/arxiv.org\/abs\/2301.09946","DOI":"10.48550\/ARXIV.2301.09946"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Dragoi, C., Henzinger, T.A., Zufferey, D.: Psync: a partially synchronous language for fault-tolerant distributed algorithms. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 400\u2013415. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837650","DOI":"10.1145\/2837614.2837650"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155\u2013173 (1982). https:\/\/doi.org\/10.1016\/0167-6423(83)90013-8","DOI":"10.1016\/0167-6423(83)90013-8"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Garc\u00eda-P\u00e9rez, \u00c1., Gotsman, A., Meshman, Y., Sergey, I.: Paxos consensus, deconstructed and abstracted. In: Ahmed, A. (ed.) Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10801, pp. 912\u2013939. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_32","DOI":"10.1007\/978-3-319-89884-1_32"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Garc\u00eda-P\u00e9rez, \u00c1., Gotsman, A., Meshman, Y., Sergey, I.: Paxos consensus, deconstructed and abstracted (extended version). CoRR abs\/1802.05969 (2018), http:\/\/arxiv.org\/abs\/1802.05969","DOI":"10.1007\/978-3-319-89884-1_32"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"von Gleissenthall, K., Kici, R.G., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony: synchronous verification of asynchronous distributed programs. Proc. ACM Program. Lang. 3(POPL), 59:1\u201359:30 (2019). https:\/\/doi.org\/10.1145\/3290372","DOI":"10.1145\/3290372"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Golab, W.M., Higham, L., Woelfel, P.: Linearizable implementations do not suffice for randomized distributed computation. In: Fortnow, L., Vadhan, S.P. (eds.) Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011. pp. 373\u2013382. ACM (2011). https:\/\/doi.org\/10.1145\/1993636.1993687","DOI":"10.1145\/1993636.1993687"},{"key":"13_CR16","unstructured":"Gray, J., Lamport, L.: Consensus on transaction commit. CoRR cs.DC\/0408036 (2004), http:\/\/arxiv.org\/abs\/cs.DC\/0408036"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving practical distributed systems correct. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015. pp. 1\u201317. ACM (2015). https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"13_CR18","unstructured":"Howard, H., Malkhi, D., Spiegelman, A.: Flexible paxos: Quorum intersection revisited. CoRR abs\/1608.06696 (2016), http:\/\/arxiv.org\/abs\/1608.06696"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Junqueira, F.P., Reed, B.C., Serafini, M.: Zab: High-performance broadcast for primary-backup systems. In: Proceedings of the 2011 IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2011, Hong Kong, China, June 27-30 2011. pp. 245\u2013256. IEEE Compute Society (2011). https:\/\/doi.org\/10.1109\/DSN.2011.5958223","DOI":"10.1109\/DSN.2011.5958223"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Kragl, B., Enea, C., Henzinger, T.A., Mutluergil, S.O., Qadeer, S.: Inductive sequentialization of asynchronous programs. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020. pp. 227\u2013242. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385980","DOI":"10.1145\/3385412.3385980"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133\u2013169 (1998). https:\/\/doi.org\/10.1145\/279227.279229","DOI":"10.1145\/279227.279229"},{"key":"13_CR22","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002), http:\/\/research.microsoft.com\/users\/lamport\/tla\/book.html"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Fast paxos. Distributed Comput. 19(2), 79\u2013103 (2006). https:\/\/doi.org\/10.1007\/s00446-006-0005-x","DOI":"10.1007\/s00446-006-0005-x"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Byzantizing paxos by refinement. In: Peleg, D. (ed.) Distributed Computing - 25th International Symposium, DISC 2011, Rome, Italy, September 20-22, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06950, pp. 211\u2013224. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24100-0_22","DOI":"10.1007\/978-3-642-24100-0_22"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a06355, pp. 348\u2013370. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"13_CR26","unstructured":"Malkhi, D., Lamport, L., Zhou, L.: Stoppable paxos. Tech. Rep. MSR-TR-2008-192 (April 2008)"},{"key":"13_CR27","unstructured":"Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system. Tech. rep. (2008), https:\/\/bitcoin.org\/bitcoin.pdf"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Oki, B.M., Liskov, B.: Viewstamped replication: A general primary copy. In: Dolev, D. (ed.) Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, Toronto, Ontario, Canada, August 15-17, 1988. pp. 8\u201317. ACM (1988). https:\/\/doi.org\/10.1145\/62546.62549","DOI":"10.1145\/62546.62549"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA), 108:1\u2013108:31 (2017). https:\/\/doi.org\/10.1145\/3140568","DOI":"10.1145\/3140568"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Krintz, C., Berger, E.D. (eds.) Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. pp. 614\u2013630. ACM (2016). https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"13_CR31","unstructured":"van Renesse, R.: Asynchronous consensus without rounds. CoRR abs\/1908.10716 (2019), http:\/\/arxiv.org\/abs\/1908.10716"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"van Renesse, R., Schiper, N., Schneider, F.B.: Vive la diff\u00e9rence: Paxos vs. viewstamped replication vs. zab. IEEE Trans. Dependable Secur. Comput. 12(4), 472\u2013484 (2015). https:\/\/doi.org\/10.1109\/TDSC.2014.2355848","DOI":"10.1109\/TDSC.2014.2355848"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Song, Y.J., van Renesse, R., Schneider, F.B., Dolev, D.: The building blocks of consensus. In: Rao, S., Chatterjee, M., Jayanti, P., Murthy, C.S.R., Saha, S.K. (eds.) Distributed Computing and Networking, 9th International Conference, ICDCN 2008, Kolkata, India, January 5-8, 2008. Lecture Notes in Computer Science, vol.\u00a04904, pp. 54\u201372. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-77444-0_5","DOI":"10.1007\/978-3-540-77444-0_5"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Wang, Z., Zhao, C., Mu, S., Chen, H., Li, J.: On the parallels between paxos and raft, and how to port optimizations. In: Robinson, P., Ellen, F. (eds.) Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, Toronto, ON, Canada, July 29 - August 2, 2019. pp. 445\u2013454. ACM (2019). https:\/\/doi.org\/10.1145\/3293611.3331595","DOI":"10.1145\/3293611.3331595"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. pp. 357\u2013368. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.E.: Planning for change in a formal verification of the raft consensus protocol. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016. pp. 154\u2013165. ACM (2016). https:\/\/doi.org\/10.1145\/2854065.2854081","DOI":"10.1145\/2854065.2854081"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Yin, M., Malkhi, D., Reiter, M.K., Golan-Gueta, G., Abraham, I.: Hotstuff: BFT consensus with linearity and responsiveness. In: Robinson, P., Ellen, F. (eds.) Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, Toronto, ON, Canada, July 29 - August 2, 2019. pp. 347\u2013356. ACM (2019). https:\/\/doi.org\/10.1145\/3293611.3331591","DOI":"10.1145\/3293611.3331591"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30044-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T09:04:26Z","timestamp":1686128666000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30044-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031300431","9783031300448"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30044-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"55","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}