Document Open Access Logo

Programming Language Abstractions for Modularly Verified Distributed Systems

Authors James R. Wilcox, Ilya Sergey, Zachary Tatlock

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2017.19.pdf
  • Filesize: 0.55 MB
  • 12 pages

Document Identifiers

Author Details

James R. Wilcox
Ilya Sergey
Zachary Tatlock

Cite As Get BibTex

James R. Wilcox, Ilya Sergey, and Zachary Tatlock. Programming Language Abstractions for Modularly Verified Distributed Systems. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 19:1-19:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.SNAPL.2017.19

Abstract

Distributed systems are rarely developed as monolithic programs. Instead, like any software, these systems may consist of multiple program components, which are then compiled separately and linked together. Modern systems also incorporate various services interacting with each other and with client applications. However, state-of-the-art verification tools focus predominantly on verifying standalone, closed-world protocols or systems, thus failing to account for the compositional nature of distributed systems. For example, standalone verification has the drawback that when protocols and their optimized implementations evolve, one must re-verify the entire system from scratch, instead of leveraging compositionality to contain the reverification effort.

In this paper, we focus on the challenge of modular verification of distributed systems with respect to high-level protocol invariants as well as for low-level implementation safety properties. We argue that the missing link between the two is a programming paradigm that would allow one to reason about both high-level distributed protocols and low-level implementation primitives in a single verification-friendly framework. Such a link would make it possible to reap the benefits from both the vast body of research in distributed computing, focused on modular protocol decomposition and consistency properties, as well as from the recent advances in program verification, enabling construction of provably correct systems implementations. To showcase the modular verification challenges, we present some typical scenarios of decomposition between a distributed protocol and its implementations. We then describe our ongoing research agenda, in which we are attempting to address the outlined problems by providing a typing discipline and a set of domain-specific primitives for specifying, implementing and verifying distributed systems. Our approach, mechanized within a proof assistant, provides the means of decomposition necessary for modular proofs about distributed protocols and systems.

Subject Classification

Keywords
  • Distributed systems
  • program verification
  • distributed protocols
  • domain-specific languages
  • type systems
  • dependent types
  • program logics.

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Martín Abadi and Leslie Lamport. The existence of refinement mappings. In LICS, pages 165-175. IEEE Computer Society, 1988. Google Scholar
  2. Romain Boichat, Partha Dutta, Svend Frølund, and Rachid Guerraoui. Deconstructing paxos. SIGACT News, 34(1):47-67, 2003. Google Scholar
  3. Marco Carbone, Fabrizio Montesi, and Carsten Schürmann. Choreographies, logically. In CONCUR, pages 47-62. Springer, 2014. Google Scholar
  4. Tushar Deepak Chandra, Robert Griesemer, and Joshua Redstone. Paxos made live: an engineering perspective. In PODC, pages 398-407. ACM, 2007. Google Scholar
  5. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using crash hoare logic for certifying the FSCQ file system. In SOSP, pages 18-37. ACM, 2015. Google Scholar
  6. Coq Development Team. The Coq Proof Assistant Reference Manual - Version 8.5pl3, 2016. URL: http://coq.inria.fr.
  7. Anupam Datta, Ante Derek, John C. Mitchell, and Arnab Roy. Protocol composition logic (PCL). Electr. Notes Theor. Comput. Sci., 172:311-358, 2007. Google Scholar
  8. Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In POPL, pages 435-446. ACM, 2011. Google Scholar
  9. Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. Concurrent Abstract Predicates. In ECOOP, volume 6183 of LNCS, pages 504-528. Springer, 2010. Google Scholar
  10. Cezara Drăgoi, Thomas A. Henzinger, and Damien Zufferey. The Need for Language Support for Fault-Tolerant Distributed Systems. In SNAPL, volume 32 of LIPIcs, pages 90-102. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  11. Cezara Drăgoi, Thomas A. Henzinger, and Damien Zufferey. PSync: a partially synchronous language for fault-tolerant distributed algorithms. In POPL, pages 400-415. ACM, 2016. Google Scholar
  12. Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. A calculus of atomic actions. In POPL, pages 2-15. ACM, 2009. Google Scholar
  13. Tzilla Elrad and Nissim Francez. Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program., 2(3):155-173, 1982. Google Scholar
  14. Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. Theor. Comput. Sci., 411(51-52):4379-4398, 2010. Google Scholar
  15. Colin S. Gordon. Verifying Concurrent Programs by Controlling Alias Interference. PhD thesis, University of Washington, 2014. Google Scholar
  16. Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. IronFleet: proving practical distributed systems correct. In SOSP, pages 1-17. ACM, 2015. Google Scholar
  17. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463-492, 1990. Google Scholar
  18. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP, volume 1381 of LNCS, pages 122-138. Springer, 1998. Google Scholar
  19. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, pages 273-284. ACM, 2008. Google Scholar
  20. Mauro Jaskelioff and Stephan Merz. Proving the correctness of disk paxos. Archive of Formal Proofs, 2005. URL: https://www.isa-afp.org/entries/DiskPaxos.shtml.
  21. Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596-619, 1983. Google Scholar
  22. Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, and Amin M. Vahdat. Mace: Language support for building distributed systems. In PLDI, pages 179-188. ACM, 2007. Google Scholar
  23. Leslie Lamport. The part-time parliament. ACM Trans. Comput. Syst., 16(2):133-169, 1998. Google Scholar
  24. Leslie Lamport. Fast paxos. Distributed Computing, 19(2):79-103, 2006. Google Scholar
  25. Leslie Lamport and Fred B. Schneider. Formal foundation for specification and verification. In Distributed Systems: Methods and Tools for Specification, An Advanced Course, volume 190 of LNCS, pages 203-285. Springer, 1985. Google Scholar
  26. Butler W. Lampson. How to build a highly available system using consensus. In WDAG, volume 1151 of LNCS, pages 1-17. Springer, 1996. Google Scholar
  27. Mohsen Lesani, Christian J. Bell, and Adam Chlipala. Chapar: certified causally consistent distributed key-value stores. In POPL, pages 357-370. ACM, 2016. Google Scholar
  28. Ruy Ley-Wild and Aleksandar Nanevski. Subjective auxiliary state for coarse-grained concurrency. In POPL, pages 561-574. ACM, 2013. Google Scholar
  29. Hongjin Liang and Xinyu Feng. Modular verification of linearizability with non-fixed linearization points. In PLDI, pages 459-470. ACM, 2013. Google Scholar
  30. Hongjin Liang, Xinyu Feng, and Ming Fu. A rely-guarantee-based simulation for verifying concurrent program transformations. In POPL, pages 455-468, 2012. Google Scholar
  31. Richard J. Lipton. Reduction: A method of proving properties of parallel programs. Commun. ACM, 18(12):717-721, 1975. Google Scholar
  32. Yanhong A. Liu, Scott D. Stoller, Bo Lin, and Michael Gorbovitski. From clarity to efficiency for distributed algorithms. In OOPSLA, pages 395-410, New York, NY, USA, 2012. ACM. Google Scholar
  33. Giuliano Losa, Sebastiano Peluso, and Binoy Ravindran. Brief announcement: A family of leaderless generalized-consensus algorithms. In PODC, pages 345-347. ACM, 2016. Google Scholar
  34. Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers Inc., 1996. Google Scholar
  35. Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In PODC, pages 137-151. ACM, 1987. Google Scholar
  36. Nancy A. Lynch and Mark R. Tuttle. An introduction to input/output automata. CWI Quarterly, 2:219-246, 1989. Google Scholar
  37. Nancy A. Lynch and Frits W. Vaandrager. Forward and backward simulations: I. untimed systems. Inf. Comput., 121(2):214-233, 1995. Google Scholar
  38. Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3):348-375, 1978. Google Scholar
  39. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I, II. Inf. Comput., 100(1):1-40, 1992. Google Scholar
  40. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. Communicating state transition systems for fine-grained concurrent resources. In ESOP, volume 8410 of LNCS, pages 290-310. Springer, 2014. Google Scholar
  41. Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in Hoare Type Theory. In ICFP, pages 62-73. ACM, 2006. Google Scholar
  42. Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Dependent types for imperative programs. In ICFP, pages 229-240. ACM Press, 2008. Google Scholar
  43. Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. Structuring the verification of heap-manipulating programs. In POPL, pages 261-274. ACM, 2010. Google Scholar
  44. Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. How Amazon web services uses formal methods. Commun. ACM, 58(4):66-73, 2015. Google Scholar
  45. Gian Ntzik, Pedro da Rocha Pinto, and Philippa Gardner. Fault-tolerant resource reasoning. In APLAS, volume 9458 of LNCS, pages 169-188. Springer, 2015. Google Scholar
  46. Diego Ongaro and John K. Ousterhout. In search of an understandable consensus algorithm. In USENIX Annual Technical Conference, pages 305-319. USENIX Association, 2014. Google Scholar
  47. Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. In PLDI, pages 614-630. ACM, 2016. Google Scholar
  48. Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable. Formal specification, verification, and implementation of fault-tolerant systems using EventML. In AVOCS. EASST, 2015. Google Scholar
  49. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS, pages 55-74. IEEE Computer Society, 2002. Google Scholar
  50. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized verification of fine-grained concurrent programs. In PLDI, pages 77-87. ACM, 2015. Google Scholar
  51. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Specifying and verifying concurrent algorithms with histories and subjectivity. In ESOP, volume 9032, pages 333-358. Springer, 2015. Google Scholar
  52. Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco. Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. In OOPSLA, pages 92-110. ACM, 2016. Google Scholar
  53. Tim Sheard, Aaron Stump, and Stephanie Weirich. Language-based verification will change the world. In FoSER, pages 343-348. ACM, 2010. Google Scholar
  54. Kasper Svendsen and Lars Birkedal. Impredicative Concurrent Abstract Predicates. In ESOP, volume 8410 of LNCS, pages 149-168. Springer, 2014. Google Scholar
  55. Bernardo Toninho, Luís Caires, and Frank Pfenning. Dependent session types via intuitionistic linear type theory. In PPDP, pages 161-172. ACM, 2011. Google Scholar
  56. Aaron Turon, Derek Dreyer, and Lars Birkedal. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP, pages 377-390. ACM, 2013. Google Scholar
  57. Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. GPS: navigating weak memory with ghosts, protocols, and separation. In OOPSLA, pages 691-707. ACM, 2014. Google Scholar
  58. Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. Logical relations for fine-grained concurrency. In POPL, pages 343-356. ACM, 2013. Google Scholar
  59. Aaron Joseph Turon and Mitchell Wand. A separation logic for refining concurrent objects. In POPL, pages 247-258. ACM, 2011. Google Scholar
  60. Viktor Vafeiadis and Matthew J. Parkinson. A Marriage of Rely/Guarantee and Separation Logic. In CONCUR, volume 4703, pages 256-271. Springer, 2007. Google Scholar
  61. Robbert van Renesse and Deniz Altinbuken. Paxos made moderately complex. ACM Comput. Surv., 47(3):42:1-42:36, 2015. Google Scholar
  62. Robbert van Renesse, Nicolas Schiper, and Fred B. Schneider. Vive la différence: Paxos vs. viewstamped replication vs. zab. IEEE Trans. Dependable Sec. Comput., 12(4):472-484, 2015. Google Scholar
  63. Gerhard Weikum and Gottfried Vossen. Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery. Morgan Kaufmann, 2002. Google Scholar
  64. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. Verdi: a framework for implementing and formally verifying distributed systems. In PLDI, pages 357-368. ACM, 2015. Google Scholar
  65. Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas E. Anderson. Planning for change in a formal verification of the Raft Consensus Protocol. In CPP, pages 154-165. ACM, 2016. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact