Document Open Access Logo

Synchronizing the Asynchronous

Authors Bernhard Kragl , Shaz Qadeer, Thomas A. Henzinger

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.21.pdf
  • Filesize: 0.7 MB
  • 17 pages

Document Identifiers

Author Details

Bernhard Kragl
  • IST Austria
Shaz Qadeer
  • Microsoft
Thomas A. Henzinger
  • IST Austria

Funding

This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).

Cite AsGet BibTex

Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. Synchronizing the Asynchronous. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.21

Abstract

Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent computation threads. We present synchronization, a new proof rule that simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Modular verification is enabled via pending asynchronous calls in atomic summaries, and a complementary proof rule that eliminates pending asynchronous calls when components and their specifications are composed. We evaluate synchronization in the context of a multi-layer refinement verification methodology on a collection of benchmark programs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • concurrent programs
  • asynchronous programs
  • deductive verification
  • refinement
  • synchronization
  • mover types
  • atomic action
  • commutativity
  • Lipton reduction

Metrics

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

References

  1. Alexander Bakst, Klaus von Gleissenthall, Rami Gökhan Kici, and Ranjit Jhala. Verifying distributed programs via canonical sequentialization. In OOPSLA, 2017. URL: http://dx.doi.org/10.1145/3133934.
  2. Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, and Serdar Tasiran. Verifying robustness of event-driven asynchronous programs against concurrency. In ESOP, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54434-1_7.
  3. Leonardo de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In TACAS, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78800-3_24.
  4. Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. PSync: a partially synchronous language for fault-tolerant distributed algorithms. In POPL, 2016. URL: http://dx.doi.org/10.1145/2837614.2837650.
  5. Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. A calculus of atomic actions. In POPL, 2009. URL: http://dx.doi.org/10.1145/1480881.1480885.
  6. Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. In PLDI, 2003. URL: http://dx.doi.org/10.1145/781131.781169.
  7. Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis. Rely/guarantee reasoning for asynchronous programs. In CONCUR, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.483.
  8. 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, 2015. URL: http://dx.doi.org/10.1145/2815400.2815428.
  9. Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran. Automated and modular refinement reasoning for concurrent programs. In CAV, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21668-3_26.
  10. Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran. Automated and modular refinement reasoning for concurrent programs. Technical Report MSR-TR-2015-8, Microsoft Research, February 2015. URL: https://www.microsoft.com/en-us/research/publication/automated-and-modular-refinement-reasoning-for-concurrent-programs/.
  11. Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. Asynchronous liquid separation types. In ECOOP, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2015.396.
  12. Bernhard Kragl and Shaz Qadeer. Layered concurrent programs. In CAV, 2018. URL: http://dx.doi.org/10.1007/978-3-319-96145-3_5.
  13. Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. Google Scholar
  14. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR, 2010. URL: http://dx.doi.org/10.1007/978-3-642-17511-4_20.
  15. Richard J. Lipton. Reduction: A method of proving properties of parallel programs. Commun. ACM, 18(12):717-721, 1975. URL: http://dx.doi.org/10.1145/361227.361234.
  16. Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271-307, 2007. URL: http://dx.doi.org/10.1016/j.tcs.2006.12.035.
  17. Wytse Oortwijn, Stefan Blom, and Marieke Huisman. Future-based static analysis of message passing programs. In PLACES, 2016. URL: http://dx.doi.org/10.4204/EPTCS.211.7.
  18. Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. In PLDI, 2016. URL: http://dx.doi.org/10.1145/2908080.2908118.
  19. Ilya Sergey, James R. Wilcox, and Zachary Tatlock. Programming and proving with distributed protocols. In POPL, 2018. URL: http://dx.doi.org/10.1145/3158116.
  20. Alexander J. Summers and Peter Müller. Actor services - modular verification of message passing programs. In ESOP, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49498-1_27.
  21. 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, 2015. URL: http://dx.doi.org/10.1145/2737924.2737958.
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 Imprint Privacy Contact