Article

A Logic-Based Framework for Verifying Consensus Algorithms

Authors:

Cezara DrăźGoi,

Thomas A. Henzinger,

Damien ZuffereyAuthors Info & Claims

VMCAI 2014: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318

Pages 161 - 181

https://doi.org/10.1007/978-3-642-54013-4_10

Published: 19 January 2014 Publication History

Abstract

Fault-tolerant distributed algorithms play an important role in ensuring the reliability of many software applications. In this paper we consider distributed algorithms whose computations are organized in rounds. To verify the correctness of such algorithms, we reason about i properties such as invariants of the state, ii the transitions controlled by the algorithm, and iii the communication graph. We introduce a logic that addresses these points, and contains set comprehensions with cardinality constraints, function symbols to describe the local states of each process, and a limited form of quantifier alternation to express the verification conditions. We show its use in automating the verification of consensus algorithms. In particular, we give a semi-decision procedure for the unsatisfiability problem of the logic and identify a decidable fragment. We successfully applied our framework to verify the correctness of a variety of consensus algorithms tolerant to both benign faults message loss, process crashes and value faults message corruption.

References

[1]

Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems 1996

[2]

Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 15, 307---309 1986

Digital Library

[3]

Ben-Or, M.: Another advantage of free choice extended abstract: Completely asynchronous agreement protocols. In: PODC, pp. 27---30. ACM 1983

Digital Library

[4]

Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: PODC, pp. 244---253 2007

Digital Library

[5]

Bouajjani, A., Dră goi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. eds. CONCUR 2009. LNCS, vol. 5710, pp. 178---195. Springer, Heidelberg 2009

Digital Library

[6]

Bradley, A.R., Manna, Z., Sipma, H.B.: What's decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. eds. VMCAI 2006. LNCS, vol. 3855, pp. 427---442. Springer, Heidelberg 2006

Digital Library

[7]

Brasileiro, F., Greve, F.G.P., Mostéfaoui, A., Raynal, M.: Consensus in one communication step. In: Malyshkin, V.E. ed. PaCT 2001. LNCS, vol. 2127, pp. 42---50. Springer, Heidelberg 2001

Digital Library

[8]

Burrows, M.: The chubby lock service for loosely-coupled distributed systems. In: OSDI. USENIX Association, Berkeley 2006

Digital Library

[9]

Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in the heard-of model. Int. J. Software and Informatics 32-3, 273---303 2009

[10]

Charron-Bost, B., Schiper, A.: The heard-of model: computing in distributed systems with benign faults. Distributed Computing 221, 49---71 2009

Digital Library

[11]

Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 322, 374---382 1985

Digital Library

[12]

Függer, M., Schmid, U.: Reconciling fault-tolerant distributed computing and systems-on-chip. Dist. Comp. 246, 323---355 2012

Digital Library

[13]

German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM 39, 675---735 1992

Digital Library

[14]

Hunt, P., Konar, M., Junqueira, F.P., Reed, B.: Zookeeper: wait-free coordination for internet-scale systems. In: USENIXATC. USENIX Association 2010

Digital Library

[15]

John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD, pp. 201---209 2013

[16]

Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with presburger arithmetic. In: Nieuwenhuis, R. ed. CADE 2005. LNCS LNAI, vol. 3632, pp. 260---277. Springer, Heidelberg 2005

Digital Library

[17]

Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 1998

Digital Library

[18]

Lamport, L.: Distributed algorithms in TLA abstract. In: PODC 2000

Digital Library

[19]

Lynch, N.: Distributed Algorithms. Morgan Kaufman 1996

Digital Library

[20]

Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL, pp. 611---622. ACM 2011

Digital Library

[21]

de Moura, L., BjØrner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. eds. TACAS 2008. LNCS, vol. 4963, pp. 337---340. Springer, Heidelberg 2008

Digital Library

[22]

Santoro, N., Widmayer, P.: Time is not a healer. In: Cori, R., Monien, B. eds. STACS 1989. LNCS, vol. 349, pp. 304---313. Springer, Heidelberg 1989

Digital Library

[23]

Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 284, 213---214 1988

Digital Library

[24]

Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: Barthe, G., Hermenegildo, M. eds. VMCAI 2010. LNCS, vol. 5944, pp. 380---395. Springer, Heidelberg 2010

Digital Library

Cited By

Winter LBuse Fde Graaf Dvon Gleissenthall KKulahcioglu Ozkan B(2023)Randomized Testing of Byzantine Fault Tolerant AlgorithmsProceedings of the ACM on Programming Languages10.1145/35860537:OOPSLA1(757-788)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586053
Zhai SLi XGe NGrundy J(2023)HOME: Heard-of Based Formal Modeling and Verification Environment for Consensus ProtocolsProceedings of the 45th International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion58688.2023.00016(16-20)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE-Companion58688.2023.00016
Jaber NWagner CJacobs SKulkarni MSamanta R(2021)QuickSilver: modeling and parameterized verification for distributed agreement-based systemsProceedings of the ACM on Programming Languages10.1145/34855345:OOPSLA(1-31)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485534
Show More Cited By

Recommendations

A counterexample guided abstraction refinement framework for verifying concurrent c programs
A Framework for Verifying Depth-First Search Algorithms
CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

Many graph algorithms are based on depth-first search (DFS). The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL.

Building on the Isabelle Refinement Framework,...
Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications

In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

VMCAI 2014: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318

January 2014

491 pages

ISBN:9783642540127

Editors:
Kenneth Mcmillan
One Microsoft Way, Microsoft Research, Redmond, USA
,
Xavier Rival
DI - Ecole Normale Supérieure, Paris Cedex 05, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 19 January 2014

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Winter LBuse Fde Graaf Dvon Gleissenthall KKulahcioglu Ozkan B(2023)Randomized Testing of Byzantine Fault Tolerant AlgorithmsProceedings of the ACM on Programming Languages10.1145/35860537:OOPSLA1(757-788)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586053
Zhai SLi XGe NGrundy J(2023)HOME: Heard-of Based Formal Modeling and Verification Environment for Consensus ProtocolsProceedings of the 45th International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion58688.2023.00016(16-20)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE-Companion58688.2023.00016
Jaber NWagner CJacobs SKulkarni MSamanta R(2021)QuickSilver: modeling and parameterized verification for distributed agreement-based systemsProceedings of the ACM on Programming Languages10.1145/34855345:OOPSLA(1-31)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485534
Le Brun MAttard DFrancalanza AAronis SBieniusa A(2021)Graft: general purpose raft consensus in ElixirProceedings of the 20th ACM SIGPLAN International Workshop on Erlang10.1145/3471871.3472963(2-14)Online publication date: 18-Aug-2021
https://dl.acm.org/doi/10.1145/3471871.3472963
Stoilkovska IKonnov IWidder JZuleger F(2021)Eliminating Message Counters in Synchronous Threshold AutomataVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_10(196-218)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1007/978-3-030-67067-2_10
Vukotic IRahli VEsteves-Veríssimo P(2019)Asphalion: trustworthy shielding against Byzantine faultsProceedings of the ACM on Programming Languages10.1145/33605643:OOPSLA(1-32)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360564
Letychevskyi OPeschanenko VRadchenko VOrlovsky MSobol A(2019)Algebraic Approach to Verification and Testing of Distributed ApplicationsProceedings of the 1st International Electronics Communication Conference10.1145/3343147.3343159(37-43)Online publication date: 7-Jul-2019
https://dl.acm.org/doi/10.1145/3343147.3343159
v. Gleissenthall KKıcı RBakst AStefan DJhala R(2019)Pretend synchrony: synchronous verification of asynchronous distributed programsProceedings of the ACM on Programming Languages10.1145/32903723:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290372
Taube MLosa GMcMillan KPadon OSagiv MShoham SWilcox JWoos D(2018)Modularity for decidability of deductive verification with applications to distributed systemsACM SIGPLAN Notices10.1145/3296979.319241453:4(662-677)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192414
Taube MLosa GMcMillan KPadon OSagiv MShoham SWilcox JWoos DFoster JGrossman D(2018)Modularity for decidability of deductive verification with applications to distributed systemsProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192414(662-677)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192414
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents