research-article

Cardinalities and universal quantifiers for verifying parameterized systems

Authors:

Klaus v. Gleissenthall,

Nikolaj Bjørner,

Andrey RybalchenkoAuthors Info & Claims

PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 599 - 613

https://doi.org/10.1145/2908080.2908129

Published: 02 June 2016 Publication History

Abstract

Parallel and distributed systems rely on intricate protocols to manage shared resources and synchronize, i.e., to manage how many processes are in a particular state. Effective verification of such systems requires universally quantification to reason about parameterized state and cardinalities tracking sets of processes, messages, failures to adequately capture protocol logic. In this paper we present Tool, an automatic invariant synthesis method that integrates cardinality-based reasoning and universal quantification. The resulting increase of expressiveness allows Tool to verify, for the first time, a representative collection of intricate parameterized protocols.

References

[1]

P. A. Abdulla, G. Delzanno, and A. Rezine. Parameterized verification of infinite-state processes with global conditions. In CAV, 2007.

Digital Library

[2]

F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina. An extension of lazy abstraction with interpolation for programs with arrays. FMSD, 45(1), 2014a. F. Alberti, S. Ghilardi, and N. Sharygina. A framework for the verification of parameterized infinite-state systems. In CILC, 2014b. F. Alberti, S. Ghilardi, and N. Sharygina. Decision procedures for flat array properties. J. Autom. Reasoning, 54(4), 2015.

Digital Library

[3]

F. Alberti, S. Ghilardi, and E. Pagani. Counting constraints in flat array fragments. In IJCAR, 2016.

Digital Library

[4]

I. Balaban, Y. Fang, A. Pnueli, and L. D. Zuck. IIV: an invisible invariant verifier. In CAV, 2005.

Digital Library

[5]

I. Balaban, A. Pnueli, and L. D. Zuck. Invisible safety of distributed protocols. In ICALP, 2006.

Digital Library

[6]

G. Basler, M. Mazzucchi, T. Wahl, and D. Kroening. Symbolic counter abstraction for concurrent software. In CAV, 2009a. G. Basler, M. Mazzucchi, T. Wahl, and D. Kroening. Symbolic counter abstraction for concurrent software. In CAV, 2009b. T. A. Beyene, C. Popeea, and A. Rybalchenko. Solving existentially quantified horn clauses. In CAV, 2013.

Digital Library

[7]

N. Bjørner, K. McMillan, and A. Rybalchenko. On solving universally quantified horn clauses. In SAS, 2013.

[8]

A. R. Bradley, Z. Manna, and H. B. Sipma. What’s decidable about arrays. In VMCAI, 2006.

[9]

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

Digital Library

[10]

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

[11]

C. Drăgoi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey. A logic-based framework for verifying consensus algorithms. In VMCAI, 2014.

Digital Library

[12]

Y. Fang, N. Piterman, A. Pnueli, and L. D. Zuck. Liveness with invisible ranking. STTT, 8(3), 2006.

[13]

A. Farzan and Z. Kincaid. Verification of parameterized concurrent programs by modular reasoning about data and control. In POPL, 2012.

Digital Library

[14]

A. Farzan, Z. Kincaid, and A. Podelski. Proofs that count. In POPL, 2014.

Digital Library

[15]

A. Farzan, Z. Kincaid, and A. Podelski. Proof spaces for unbounded parallelism. In POPL, 2015.

Digital Library

[16]

M. Fredrikson and S. Jha. Satisfiability modulo counting: A new approach for analyzing privacy properties. In LICS, 2014.

Digital Library

[17]

Z. Ganjei, A. Rezine, P. Eles, and Z. Peng. Abstracting and counting synchronizing processes. In VMCAI, 2015.

Digital Library

[18]

S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, 2012.

Digital Library

[19]

S. Gulwani, B. McCloskey, and A. Tiwari. Lifting abstract interpreters to quantified logical domains. In POPL, 2008.

Digital Library

[20]

S. Gulwani, T. Lev-Ami, and M. Sagiv. A combination framework for tracking partition sizes. In POPL. ACM, 2009.

Digital Library

[21]

C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill. IronFleet: Proving practical distributed systems correct. In SOSP, 2015a. C. Hawblitzel, E. Petrank, S. Qadeer, and S. Tasiran. Automated and modular refinement reasoning for concurrent programs. In CAV, 2015b. M. Heizmann, J. Hoenicke, and A. Podelski. Refinement of trace abstraction. In SAS, 2009.

Digital Library

[22]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, 2002.

Digital Library

[23]

T. A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In PLDI, 2004a. T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL, 2004b. M. Herlihy and N. Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008.

Digital Library

[24]

K. Hoder and N. Bjørner. Generalized property directed reachability. In SAT, 2012.

Digital Library

[25]

H. Hojjat, F. Konecný, F. Garnier, R. Iosif, V. Kuncak, and P. Rümmer. A verification toolkit for numerical transition systems - tool paper. In FM, 2012.

[26]

H. Hojjat, P. Rümmer, P. Subotic, and W. Yi. Horn clauses for communicating timed systems. In HCVS, 2014.

[27]

P. Hunt, M. Konar, F. P. Junqueira, and B. Reed. ZooKeeper: Waitfree coordination for Internet-scale systems. In USENIX, 2010.

Digital Library

[28]

T. Kahsai, J. A. Navas, A. Gurfinkel, and A. Komuravelli. The SeaHorn verification framework. In CAV, 2015.

[29]

A. Kaiser, D. Kroening, and T. Wahl. Lost in abstraction: Monotonicity in multi-threaded programs. In CONCUR, 2014.

[30]

R. Kotla, L. Alvisi, M. Dahlin, A. Clement, and E. L. Wong. Zyzzyva: speculative Byzantine fault tolerance. In SOSP, 2007.

Digital Library

[31]

D. Kroening and M. Lewis. Second-order SAT solving using program synthesis. CoRR, abs/1409.4925, 2014.

[32]

V. Kuncak, H. H. Nguyen, and M. C. Rinard. An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic. In CADE, 2005.

Digital Library

[33]

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

Digital Library

[34]

L. Lamport. Mechanically checked safety proof of a byzantine Paxos algorithm, 2015. http://research.microsoft. com/users/lamport/tla/byzpaxos.html. Concurrent Garbage Collection. .NET Framework 4.6 and 4.5. Microsoft, 2015.

[35]

https://msdn.microsoft. com/en-us/library/ee787088(v=vs.110).aspx# concurrent_garbage_collection. D. Monniaux and F. Alberti. A simple abstraction of arrays and maps by program translation. SAS, 2015.

[36]

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff. How Amazon web services uses formal methods. Commun. ACM, 2015.

Digital Library

[37]

D. Ongaro and J. Ousterhout. In search of an understandable consensus algorithm. In USENIX ATC, 2014.

Digital Library

[38]

R. Piskac and V. Kuncak. Fractional collections with cardinality bounds, and mixed linear arithmetic with stars. In CSL, 2008a. R. Piskac and V. Kuncak. Decision procedures for multisets with cardinality constraints. In VMCAI, 2008b. A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1, infty)-counter abstraction. In CAV, 2002a. A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1, infty)-counter abstraction. In CAV, 2002b. S. Qadeer, S. K. Rajamani, and J. Rehof. Summarizing procedures in concurrent programs. In POPL, 2004.

Digital Library

[39]

A. Sanchez, S. Sankaranarayanan, C. Sànchez, and B.-Y. E. Chang. Invariant generation for parametrized systems using selfreflection. In SAS, 2012.

Digital Library

[40]

I. Sergey, A. Nanevski, and A. Banerjee. Mechanized verification of fine-grained concurrent programs. In PLDI, 2015.

Digital Library

[41]

T. Terauchi and H. Unno. Relaxed stratification: A new approach to practical complete predicate refinement. In ESP, 2015.

[42]

H. Unno and T. Terauchi. Inferring simple solutions to recursionfree horn clauses via sampling. In TACAS, 2015.

Digital Library

[43]

K. v. Gleissenthall, B. Köpf, and A. Rybalchenko. Symbolic polytopes for quantitative interpolation and verification. In CAV, 2015.

[44]

K. Yessenov, R. Piskac, and V. Kuncak. Collections, cardinalities, and relations. In VMCAI, 2010.

Digital Library

[45]

L. Yongjian. A novel approach to the parameterized verification of cache coherence protocols. In Tech Report. http://lcs.ios.ac.cn/~lyj238/papers/ techReportCache.pdf. P. Zave. How to make Chord correct (using a stable base). CoRR, abs/1502.06461, 2015.

Cited By

Raya RKunčak V(2024)Succinct Ordering and Aggregation Constraints in Algebraic Array TheoriesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100978(100978)Online publication date: May-2024
https://doi.org/10.1016/j.jlamp.2024.100978
Raya RKunčak V(2024)On algebraic array theoriesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100906136(100906)Online publication date: Jan-2024
https://doi.org/10.1016/j.jlamp.2023.100906
Long TRen XWang QWang C(2022)Verifying the safety properties of distributed systems via mergeable parallelismJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2022.102646130:COnline publication date: 1-Sep-2022
https://dl.acm.org/doi/10.1016/j.sysarc.2022.102646
Show More Cited By

Index Terms

Recommendations

Cardinalities and universal quantifiers for verifying parameterized systems
PLDI '16

Parallel and distributed systems rely on intricate protocols to manage shared resources and synchronize, i.e., to manage how many processes are in a particular state. Effective verification of such systems requires universally quantification to reason ...
Mechanically Verifying Concurrent Programs with the Boyer-Moore Prove

A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an ...
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 ACM Conferences

PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2016

726 pages

ISBN:9781450342612

DOI:10.1145/2908080

General Chair:
Chandra Krintz
University of California at Santa Barbara, USA
,
Program Chair:
Emery Berger
University of Massachusetts at Amherst, USA

ACM SIGPLAN Notices Volume 51, Issue 6
PLDI '16
June 2016
726 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2980983
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 June 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '16

Sponsor:

SIGPLAN

PLDI '16: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 13 - 17, 2016

CA, Santa Barbara, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
295
Total Downloads

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

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Raya RKunčak V(2024)Succinct Ordering and Aggregation Constraints in Algebraic Array TheoriesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100978(100978)Online publication date: May-2024
https://doi.org/10.1016/j.jlamp.2024.100978
Raya RKunčak V(2024)On algebraic array theoriesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100906136(100906)Online publication date: Jan-2024
https://doi.org/10.1016/j.jlamp.2023.100906
Long TRen XWang QWang C(2022)Verifying the safety properties of distributed systems via mergeable parallelismJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2022.102646130:COnline publication date: 1-Sep-2022
https://dl.acm.org/doi/10.1016/j.sysarc.2022.102646
Ganjei ZRezine AEles PPeng Z(2021)Verifying Safety of Parameterized Heard-Of AlgorithmsNetworked Systems10.1007/978-3-030-67087-0_14(209-226)Online publication date: 14-Jan-2021
https://doi.org/10.1007/978-3-030-67087-0_14
Ghilardi SPagani E(2020)Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant SystemsJournal of Automated Reasoning10.1007/s10817-020-09578-5Online publication date: 29-Aug-2020
https://doi.org/10.1007/s10817-020-09578-5
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
Berkovits ILazić MLosa GPadon OShoham S(2019)Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable LogicsComputer Aided Verification10.1007/978-3-030-25543-5_15(245-266)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25543-5_15
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
Padon OLosa GSagiv MShoham S(2017)Paxos made EPR: decidable reasoning about distributed protocolsProceedings of the ACM on Programming Languages10.1145/31405681:OOPSLA(1-31)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3140568
Show More Cited By

View Options

Get Access

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents