Rely/Guarantee Reasoning for Asynchronous Programs

Authors Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.483.pdf
  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Author Details

Ivan Gavran
Filip Niksic
Aditya Kanade
Rupak Majumdar
Viktor Vafeiadis

Cite AsGet BibTex

Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis. Rely/Guarantee Reasoning for Asynchronous Programs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 483-496, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.483

Abstract

Asynchronous programming has become ubiquitous in smartphone and web application development, as well as in the development of server-side and system applications. Many of the uses of asynchrony can be modeled by extending programming languages with asynchronous procedure calls - procedures not executed immediately, but stored and selected for execution at a later point by a non-deterministic scheduler. Asynchronous calls induce a flow of control that is difficult to reason about, which in turn makes formal verification of asynchronous programs challenging. In response, we take a rely/guarantee approach: Each asynchronous procedure is verified separately with respect to its rely and guarantee predicates; the correctness of the whole program then follows from the natural conditions the rely/guarantee predicates have to satisfy. In this way, the verification of asynchronous programs is modularly decomposed into the more usual verification of sequential programs with synchronous calls. For the sequential program verification we use Hoare-style deductive reasoning, which we demonstrate on several simplified examples. These examples were inspired from programs written in C using the popular Libevent library; they are manually annotated and verified within the state-of-the-art Frama-C platform.
Keywords
  • Asynchronous programs
  • rely/guarantee reasoning

Metrics

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

References

  1. M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507-534, 1995. Google Scholar
  2. P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C - A software analysis perspective. In SEFM 2012, pages 233-247, 2012. Google Scholar
  3. E. D'Osualdo, J. Kochems, and C.-H. L. Ong. Automatic verification of Erlang-style concurrency. In Proceedings of the 20th Static Analysis Symposium, SAS'13. Springer-Verlag, 2013. Google Scholar
  4. J. Esparza, R. Ledesma-Garza, R. Majumdar, P. Meyer, and F. Niksic. An SMT-based approach to coverability analysis. In CAV 2014, volume 8559 of Lecture Notes in Computer Science, pages 603-619. Springer, 2014. Google Scholar
  5. C. Flanagan, S.N. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In ESOP 2002, pages 262-277, 2002. Google Scholar
  6. P. Ganty and R. Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6, 2012. Google Scholar
  7. A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL 11, pages 331-344. ACM, 2011. Google Scholar
  8. T.A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In PLDI 2004, pages 1-13. ACM, 2004. Google Scholar
  9. R. Jhala and R. Majumdar. Interprocedural analysis of asynchronous programs. In POPL 2007, pages 339-350. ACM, 2007. Google Scholar
  10. C.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
  11. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Efficient coverability analysis by proof minimization. In Proceedings of the 23rd International Conference on Concurrency Theory, CONCUR'12, pages 500-515. Springer-Verlag, 2012. Google Scholar
  12. H.C. Lauer and R.M. Needham. On the duality of operating system structures. SIGOPS Oper. Syst. Rev., 13(2):3-19, 1979. Google Scholar
  13. N. Mathewson. Fast portable non-blocking network programming with Libevent. http://www.wangafu.net/~nickm/libevent-book/. Accessed: 2015-03-12.
  14. K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In CAV'06, volume 4144 of LNCS, pages 300-314. Springer, 2006. 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