More Web Proxy on the site http://driver.im/

research-article

Open access

Pretend synchrony: synchronous verification of asynchronous distributed programs

Authors:

Klaus v. Gleissenthall,

Rami Gökhan Kıcı,

Alexander Bakst,

Ranjit JhalaAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 59, Pages 1 - 30

https://doi.org/10.1145/3290372

Published: 02 January 2019 Publication History

Abstract

We present pretend synchrony, a new approach to verifying distributed systems, based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous when verifying their correctness. To do so, we compute a synchronization, a semantically equivalent program where all sends, receives, and message buffers, have been replaced by simple assignments, yielding a program that can be verified using Floyd-Hoare style Verification Conditions and SMT. We implement our approach as a framework for writing verified distributed programs in Go and evaluate it with four challenging case studies— the classic two-phase commit protocol, the Raft leader election protocol, single-decree Paxos protocol, and a Multi-Paxos based distributed key-value store. We find that pretend synchrony allows us to develop performant systems while making verification of functional correctness simpler by reducing manually specified invariants by a factor of 6, and faster, by reducing checking time by three orders of magnitude.

Supplementary Material

WEBM File (a59-gleissenthall.webm)

Download
77.57 MB

References

[1]

Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal dynamic partial order reduction. In ACM SIGPLAN Notices, Vol. 49. ACM, 373–384.

Digital Library

[2]

Alexander Bakst, Klaus von Gleissenthall, Rami Gökhan Kici, and Ranjit Jhala. 2017. Verifying distributed programs via canonical sequentialization. PACMPL 1, OOPSLA (2017), 110:1–110:27.

Digital Library

[3]

Arthur J. Bernstein. 1966. Analysis of Programs for Parallel Processing. IEEE Trans. Electronic Computers 15, 5 (1966), 757–763.

[4]

Nikolaj Bjørner, Ken McMillan, and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS.

[5]

Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. 2018. On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II . 372–391.

[6]

Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What’s Decidable About Arrays?. In VMCAI.

[7]

Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz. 2009. A Reduction Theorem for the Verification of Round-Based Distributed Algorithms. In Reachability Problems, 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings . 93–106.

Digital Library

[8]

Minas Charalambides, Peter Dinges, and Gul Agha. 2016. Parameterized, concurrent session types for asynchronous multi-actor interactions. Science of Computer Programming 115 (2016), 100–126.

Digital Library

[9]

Ernie Cohen and Leslie Lamport. 1998. Reduction in TLA. In CONCUR ’98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings . 317–331.

Digital Library

[10]

Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. 2012. Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4 (2012).

[11]

Ankush Desai, Pranav Garg, and P. Madhusudan. 2014. Natural proofs for asynchronous programs using almost-synchronous reductions. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014 . 709–725.

Digital Library

[12]

Ankush Desai, Shaz Qadeer, and Sanjit A. Seshia. 2015. Systematic testing of asynchronous reactive systems. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2015, Bergamo, Italy, August 30 - September 4, 2015 . 73–83.

Digital Library

[13]

E. D’Osualdo, J. Kochems, and C.-H. L. Ong. 2013. Automatic Verification of Erlang-Style Concurrency. In Proceedings of the 20th Static Analysis Symposium (SAS’13) . Springer-Verlag.

[14]

Emanuele D’Osualdo, Jonathan Kochems, and Luke Ong. 2012. Soter: An Automatic Safety Verifier for Erlang. In Proceedings of the 2Nd Edition on Programming Systems, Languages and Applications Based on Actors, Agents, and Decentralized Control Abstractions (AGERE! 2012) . ACM, New York, NY, USA, 137–140.

Digital Library

[15]

Cezara Drăgoi, Thomas A Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. 2014. A logic-based framework for verifying consensus algorithms. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 161–181.

Digital Library

[16]

Cezara Drăgoi, Thomas A Henzinger, and Damien Zufferey. 2016. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. ACM SIGPLAN Notices 51, 1 (2016), 400–415.

Digital Library

[17]

C. Dragoi and J. Widder. 2018. Reducing asynchrony to synchronized rounds. ArXiv e-prints (April 2018). arXiv: cs.PL/1804.07078

[18]

Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. 2009. A Calculus of Atomic Actions. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’09) . ACM, New York, NY, USA, 2–15.

Digital Library

[19]

Tzilla Elrad and Nissim Francez. 1982. Decomposition of Distributed Programs into Communication-Closed Layers. Sci. Comput. Program. 2, 3 (1982), 155–173.

[20]

Manuel Fahndrich and Robert DeLine. 2002. Adoption and Focus: Practical Linear Types for Imperative Programming. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI ’02) . ACM, New York, NY, USA, 13–24.

Digital Library

[21]

Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2014. Proofs that count. ACM SIGPLAN Notices 49, 1 (2014), 151–164.

Digital Library

[22]

Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software. In ACM Sigplan Notices, Vol. 40. ACM, 110–121.

Digital Library

[23]

Cormac Flanagan and Shaz Qadeer. 2003. A type and effect system for atomicity. In ACM SIGPLAN Notices, Vol. 38. ACM, 338–349.

Digital Library

[24]

Klaus v Gleissenthall, Nikolaj Bjørner, and Andrey Rybalchenko. 2016. Cardinalities and universal quantifiers for verifying parameterized systems. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation . ACM, 599–613.

Digital Library

[25]

Patrice Godefroid, J van Leeuwen, J Hartmanis, G Goos, and Pierre Wolper. 1996. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem . Vol. 1032. Springer Heidelberg.

[26]

Arie Gurfinkel, Sharon Shoham, and Yuri Meshman. 2016. SMT-based verification of parameterized systems. In Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016 . 338–348.

Digital Library

[27]

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty, and Brian Zill. 2015a. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles . ACM, 1–17.

Digital Library

[28]

Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran. 2015b. Automated and Modular Refinement Reasoning for Concurrent Programs. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II . 449–465.

[29]

Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski. 2017. Thread modularity at many levels: a pearl in compositional verification. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 . 473–485. http://dl.acm.org/citation.cfm?id=3009893

Digital Library

[30]

Kohei Honda. 1993. Types for dyadic interaction. In CONCUR.

Digital Library

[31]

Kohei Honda, Eduardo RB Marques, Francisco Martins, Nicholas Ng, Vasco T Vasconcelos, and Nobuko Yoshida. 2012. Verification of MPI programs using session types. In European MPI Users’ Group Meeting. Springer, 291–293.

Digital Library

[32]

Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In POPL.

Digital Library

[33]

Charles Edwin Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. 2007. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In 4th Symposium on Networked Systems Design and Implementation (NSDI 2007), April 11-13, 2007, Cambridge, Massachusetts, USA, Proceedings.

Digital Library

[34]

Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder. 2017. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages . ACM, 719–734.

Digital Library

[35]

Igor Konnov, Helmut Veith, and Josef Widder. 2015. SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms. In International Conference on Computer Aided Verification. Springer, 85–102.

[36]

Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. 2018. Synchronizing the Asynchronous. In CONCUR.

[37]

Leslie Lamport. 2001. Paxos Made Simple. (December 2001), 51–58. https://www.microsoft.com/en-us/research/publication/ paxos-made-simple/

[38]

Leslie Lamport, Dahlia Malkhi, and Lidong Zhou. 2008. Stoppable Paxos. Technical Report. Microsoft Research.

[39]

Butler Lampson and Howard E. Sturgis. 1976. Crash Recovery in a Distributed Data Storage System. In Technical report XEROX Palo Alto Research Center .

[40]

Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2018. A Static Verification Framework for Message Passing in Go using Behavioural Types. In 40th International Conference on Software Engineering. ACM, 1137–1148.

Digital Library

[41]

K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning . Springer, 348–370.

Digital Library

[42]

K. R. M. Leino and C. Pit-Claudel. 2016. Trigger selection strategies to stabilize program verifiers. In CAV.

[43]

Richard J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18, 12 (Dec. 1975), 717–721.

Digital Library

[44]

Ognjen Marić, Christoph Sprenger, and David Basin. 2017. Cutoff Bounds for Consensus Algorithms. Technical Report. CAV.

[45]

Kenneth L. McMillan. 1999. Verification of Infinite State Systems by Compositional Model Checking. In Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME ’99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings . 219–234.

Digital Library

[46]

David Monniaux and Francesco Alberti. 2015. A Simple Abstraction of Arrays and Maps by Program Translation. In Static Analysis: 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings, Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 217–234.

[47]

Iulian Moraru, David G Andersen, and Michael Kaminsky. 2013. There is More Consensus in Egalitarian Parliaments. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles (SOSP ’13) . ACM, New York, NY, USA, 358–372.

Digital Library

[48]

C. Norris IP and David L. Dill. 1996. Better verification through symmetry. Formal Methods in System Design 9, 1 (1996), 41–75.

Digital Library

[49]

Diego Ongaro and John Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (USENIX ATC’14) . USENIX Association, Berkeley, CA, USA, 305–320. http://dl.acm.org/citation.cfm?id=2643634.2643666

Digital Library

[50]

Susan Owicki and David Gries. 1976. Verifying properties of parallel programs: an axiomatic approach. In Communications of the ACM .

Digital Library

[51]

Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. 2017. Paxos made EPR: decidable reasoning about distributed protocols. PACMPL 1, OOPSLA (2017), 108:1–108:31.

Digital Library

[52]

Oded Padon, Kenneth L McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation . ACM, 614–630.

Digital Library

[53]

Amir Pnueli, Jessie Xu, and Lenore Zuck. 2002. Liveness with (0, 1, ∞)-counter abstraction. In International Conference on Computer Aided Verification . Springer, 107–122.

Digital Library

[54]

Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. 1999. Parametric Shape Analysis via 3-valued Logic. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’99) . ACM, New York, NY, USA, 105–118.

Digital Library

[55]

Alejandro Sanchez, Sriram Sankaranarayanan, César Sánchez, and Bor-Yuh Evan Chang. 2012. Invariant Generation for Parametrized Systems Using Self-reflection . Springer Berlin Heidelberg, Berlin, Heidelberg, 146–163.

Digital Library

[56]

Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming and Proving with Distributed Protocols. In POPL.

Digital Library

[57]

Ion Stoica, Robert Morris, David Karger, M. Frans Kaashoek, and Hari Balakrishnan. 2001. Chord: A Scalable Peer-topeer Lookup Service for Internet Applications. In Proceedings of the 2001 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (SIGCOMM ’01) . ACM, New York, NY, USA, 149–160.

Digital Library

[58]

Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018b. Modularity for decidability of deductive verification with applications to distributed systems. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018 . 662–677.

Digital Library

[59]

Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018a. Modularity for Decidability of Deductive Verification with Applications to Distributed Systemswith Applications to Distributed Systems. In PLDI.

Digital Library

[60]

Nissim Francez Tzilla Elrad. 1982. Decomposition of distributed programs into communication-closed layers. In Science of Computer Programming .

[61]

James R. Wilcox, Ilya Sergey, and Zachary Tatlock. 2017. Programming Language Abstractions for Modularly Verified Distributed Systems. In SNAPL.

[62]

James R Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D Ernst, and Thomas Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. In ACM SIGPLAN Notices, Vol. 50. ACM, 357–368.

Digital Library

[63]

Doug Woos, James R Wilcox, Steve Anton, Zachary Tatlock, Michael D Ernst, and Thomas Anderson. 2016. Planning for change in a formal verification of the raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs . ACM, 154–165.

Digital Library

[64]

Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou. 2009. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2009, April 22-24, 2009, Boston, MA, USA . 213–228.

Digital Library

Cited By

Lin ZGancher JParno B(2024)FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional PermissionsProceedings of the ACM on Programming Languages10.1145/36897298:OOPSLA2(499-526)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689729
Farzan AKlumpp DPodelski A(2024)Commutativity Simplifies Proofs of Parameterized ProgramsProceedings of the ACM on Programming Languages10.1145/36329258:POPL(2485-2513)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632925
Linvill KKaki GWustrow E(2023)Verifying Indistinguishability of Privacy-Preserving ProtocolsProceedings of the ACM on Programming Languages10.1145/36228497:OOPSLA2(1442-1469)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622849
Show More Cited By

Index Terms

Pretend synchrony: synchronous verification of asynchronous distributed programs
1. Software and its engineering
  1. Software notations and tools
2. Theory of computation
  1. Models of computation
    1. Concurrency
      1. Distributed computing models
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
      2. Program verification

Recommendations

Verifying distributed programs via canonical sequentialization

We introduce canonical sequentialization, a new approach to verifying unbounded, asynchronous, message-passing programs at compile-time. Our approach builds upon the following observation: due the combinatorial explosion in complexity, programmers do ...
Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Natural proofs for asynchronous programs using almost-synchronous reductions
OOPSLA '14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications

We consider the problem of provably verifying that an asynchronous message-passing system satisfies its local assertions. We present a novel reduction scheme for asynchronous event-driven programs that finds almost-synchronous invariants - invariants ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

34
Total Citations
View Citations
1,535
Total Downloads

Downloads (Last 12 months)189
Downloads (Last 6 weeks)24

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lin ZGancher JParno B(2024)FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional PermissionsProceedings of the ACM on Programming Languages10.1145/36897298:OOPSLA2(499-526)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689729
Farzan AKlumpp DPodelski A(2024)Commutativity Simplifies Proofs of Parameterized ProgramsProceedings of the ACM on Programming Languages10.1145/36329258:POPL(2485-2513)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632925
Linvill KKaki GWustrow E(2023)Verifying Indistinguishability of Privacy-Preserving ProtocolsProceedings of the ACM on Programming Languages10.1145/36228497:OOPSLA2(1442-1469)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622849
Wagner CJaber NSamanta R(2023)Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded RegionsProceedings of the ACM on Programming Languages10.1145/35860337:OOPSLA1(172-200)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586033
Di Giusto CFerré DLaversa LLozes E(2023)A Partial Order View of Message-Passing Communication ModelsProceedings of the ACM on Programming Languages10.1145/35712487:POPL(1601-1627)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571248
Farzan A(2023)Commutativity in Automated Verification2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175734(1-7)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175734
Goel ASakallah K(2023)Regularity and quantification: a new approach to verify distributed protocolsInnovations in Systems and Software Engineering10.1007/s11334-022-00460-819:4(359-377)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1007/s11334-022-00460-8
Dilley NLange J(2023)Automated verification of concurrent go programs via bounded model checkingAutomated Software Engineering10.1007/s10515-023-00391-z30:2Online publication date: 26-Aug-2023
https://dl.acm.org/doi/10.1007/s10515-023-00391-z
Lette DFarzan A(2023)Commutativity for Concurrent Program Termination ProofsComputer Aided Verification10.1007/978-3-031-37706-8_6(109-131)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_6
Cirisci BEnea CMutluergil S(2023)Quorum Tree Abstractions of Consensus ProtocolsProgramming Languages and Systems10.1007/978-3-031-30044-8_13(337-362)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_13
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents