Alexander Bakst
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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 not reason about their systems by case-splitting over all the possible execution orders. Instead, correct programs tend to be well-structured so that the programmer can reason about a small number of representative executions, which we call the program’s canonical sequentialization. We have implemented our approach in a tool called Brisk that synthesizes canonical sequentializations for programs written in Haskell, and evaluated it on a wide variety of distributed systems including benchmarks from the literature and implementations of MapReduce, two-phase commit, and a version of the Disco distributed file-system. We show that unlike model checking, which gets prohibitively slow with just 10 processes Brisk verifies the unbounded versions of the benchmarks in tens of milliseconds, yielding the first concurrency verification tool that is fast enough to be integrated into a design-implement-check cycle.
Supplemental Material
Available for Download
- Martín Abadi and Leslie Lamport. 1991. The Existence of Refinement Mappings. Theor. Comput. Sci. 82, 2 (May 1991), 253–284. Google Scholar
Digital Library
- Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal dynamic partial order reduction. In ACM SIGPLAN Notices, Vol. 49. ACM, 373–384. Google ScholarDigital Library
- Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Ying Xu, and Lenore Zuck. 2001. Parameterized Verification with Automatically Computed Inductive Assertions . Springer Berlin Heidelberg, Berlin, Heidelberg, 221–234.Google Scholar
- Samik Basu, Tevfik Bultan, and Meriem Ouederni. 2012. Synchronizability for verification of asynchronously communicating systems. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 56–71. Google ScholarDigital Library
- Nikolaj Bjørner, Ken McMillan, and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS. Google ScholarCross Ref
- Luca Cardelli. 1984. Compiling a functional language. In Proceedings of the 1984 ACM Symposium on LISP and functional programming . ACM, 208–217. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Alessandro Cimatti, Iman Narasamdya, and Marco Roveri. 2011. Boosting Lazy Abstraction for SystemC with Partial Order Reduction. In TACAS. Google ScholarCross Ref
- Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages . ACM, 238–252. Google ScholarDigital Library
- Jeffrey Dean and Sanjay Ghemawat. 2004. MapReduce: Simplified Data Processing on Large Clusters. In OSDI.Google Scholar
- Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. 2012. Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4 (2012). Google ScholarCross Ref
- Ankush Desai, Pranav Garg, and P Madhusudan. 2014. Natural proofs for asynchronous programs using almost-synchronous reductions. In ACM SIGPLAN Notices, Vol. 49. ACM, 709–725. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Disco-Project. 2017. Disco MapReduce. http://discoproject.org . (April 2017).Google Scholar
- 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. Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Jeff Epstein, Andrew P Black, and Simon Peyton-Jones. 2011. Towards Haskell in the cloud. In ACM SIGPLAN Notices, Vol. 46. ACM, 118–129.Google ScholarDigital Library
- Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2014. Proofs that count. ACM SIGPLAN Notices 49, 1 (2014), 151–164. Google ScholarDigital Library
- Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software. In ACM Sigplan Notices , Vol. 40. ACM, 110–121. Google ScholarDigital Library
- Cormac Flanagan and Shaz Qadeer. 2003. A type and effect system for atomicity. In ACM SIGPLAN Notices, Vol. 38. ACM, 338–349. Google ScholarDigital Library
- Lars-Åke Fredlund and Hans Svensson. 2007. McErlang: a model checker for a distributed functional programming language. In ACM SIGPLAN Notices, Vol. 42. ACM, 125–136. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Kohei Honda. 1993. Types for dyadic interaction. In CONCUR. Google ScholarCross Ref
- 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.Google ScholarDigital Library
- Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types.. In POPL. Google ScholarDigital Library
- Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty Asynchronous Session Types. J. ACM 63, 1, Article 9 (March 2016), 67 pages. Google ScholarDigital Library
- Frank Huch. 1999. Verification of Erlang Programs using Abstract Interpretation and Model Checking. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, September 27-29, 1999. 261–272. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- 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. Google ScholarCross Ref
- Butler Lampson and Howard E. Sturgis. 1976. Crash Recovery in a Distributed Data Storage System. In Technical report XEROX Palo Alto Research Center .Google Scholar
- Richard J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18, 12 (Dec. 1975), 717–721. Google ScholarDigital Library
- Simon Marlow. 2012. Parallel and concurrent programming in Haskell. In Central European Functional Programming School. Springer, 339–401. Google ScholarDigital Library
- 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. Google ScholarCross Ref
- Neil Mitchell and Colin Runciman. 2009. Losing functions without gaining data: another look at defunctionalisation. In Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell . ACM, 13–24. Google ScholarDigital Library
- David Monniaux and Francesco Alberti. 2015. A Simple Abstraction of Arrays and Maps by Program Translation. Springer Berlin Heidelberg, Berlin, Heidelberg, 217–234. Google ScholarCross Ref
- Nicholas Ng and Nobuko Yoshida. 2016. Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis. In CC. Google ScholarDigital Library
- C. Norris IP and David L. Dill. 1996. Better verification through symmetry. Formal Methods in System Design 9, 1 (1996), 41–75. Google ScholarDigital Library
- Dominic Orchard and Nobuko Yoshida. 2016. Effects as sessions, sessions as effects. In POPL. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Amir Pnueli, Sitvanit Ruah, and Lenore Zuck. 2001. Automatic deductive verification with invisible invariants. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 82–97. Google ScholarCross Ref
- Amir Pnueli, Jessie Xu, and Lenore Zuck. 2002. Liveness with (0, 1, ∞)-counter abstraction. In International Conference on Computer Aided Verification . Springer, 107–122. Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Stephen F Siegel. 2005. Efficient verification of halting properties for MPI programs with wildcard receives. In International Workshop on Verification, Model Checking, and Abstract Interpretation . Springer, 413–429.Google ScholarDigital Library
- Stephen F Siegel and George S Avrunin. 2005. Modeling wildcard-free MPI programs for verification. In Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming . ACM, 95–106.Google ScholarDigital Library
- Stephen F Siegel and Ganesh Gopalakrishnan. 2011. Formal analysis of message passing. In International Workshop on Verification, Model Checking, and Abstract Interpretation . Springer, 2–18.Google ScholarCross Ref
- Stephen F. Siegel and Timothy K. Zirkel. [n. d.]. Automatic Formal Verification of MPI-Based Parallel Programs. 309–310.Google Scholar
- Alexander J. Summers and Peter Müller. 2016. Actor Services. In ESOP. Google ScholarDigital Library
- Samira Tasharofi, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha. 2012. TransDPOR: A Novel Dynamic Partial-order Reduction Technique for Testing Actor Programs. In Proceedings of the 14th Joint IFIP WG 6.1 International Conference and Proceedings of the 32Nd IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems (FMOODS’12/FORTE’12) . Springer-Verlag, Berlin, Heidelberg, 219–234. Google ScholarDigital Library
- Bjorn Wachter, Daniel Kroening, and Joel Ouaknine. 2013. Verifying multi-threaded software with Impact. In Formal Methods in Computer-Aided Design (FMCAD), 2013 . IEEE, 210–217. Google ScholarCross Ref
- 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.Google ScholarDigital Library
- 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.Google ScholarDigital Library
Index Terms
- Verifying distributed programs via canonical sequentialization
Recommendations
Pretend synchrony: synchronous verification of asynchronous distributed programs
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 ...
Formal Sequentialization of Distributed Systems via Program Rewriting
Formal sequentialization is introduced as a rewriting process for the reduction of parallelism and internal communication statements of distributed imperative programs. It constructs an equivalence proof in an implicit way, via the application of ...
On the Verification of Livelock-Freedom and Self-Stabilization on Parameterized Rings
This article investigates the verification of livelock-freedom and self-stabilization on parameterized rings consisting of symmetric, constant space, deterministic, and self-disabling processes. The results of this article have a significant impact on ...
Comments