Document Open Access Logo

Modular Verification of Finite Blocking in Non-terminating Programs

Authors Pontus Boström, Peter Müller

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2015.639.pdf
  • Filesize: 0.55 MB
  • 25 pages

Document Identifiers

Author Details

Pontus Boström
Peter Müller

Cite As Get BibTex

Pontus Boström and Peter Müller. Modular Verification of Finite Blocking in Non-terminating Programs. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 639-663, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.ECOOP.2015.639

Abstract

Most multi-threaded programs synchronize threads via blocking operations such as acquiring locks or joining other threads. An important correctness property of such programs is for each thread to make progress, that is, not to be blocked forever. For programs in which all threads terminate, progress essentially follows from deadlock freedom. However, for the common case that a program contains non-terminating threads such as servers or actors, deadlock freedom is not sufficient. For instance, a thread may be blocked forever by a non-terminating thread if it attempts to join that thread or to acquire a lock held by that thread.

In this paper, we present a verification technique for finite blocking in non-terminating programs. The key idea is to track explicitly whether a thread has an obligation to perform an operation that unblocks another thread, for instance, an obligation to release a lock or to terminate. Each obligation is associated with a measure to ensure that it is fulfilled within finitely many steps. Obligations may be used in specifications, which makes verification modular. We formalize our technique via an encoding into Boogie, which treats different kinds of obligations uniformly. It subsumes termination checking as a special case.

Subject Classification

Keywords
  • Program verification
  • concurrency
  • liveness
  • progress
  • obligations

Metrics

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

References

  1. M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P. de Roever, editors, FMCO, volume 4111 of LNCS, pages 364-387. Springer, 2005. Google Scholar
  2. B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi. Proving that programs eventually do something good. In POPL, pages 265-276. ACM, 2007. Google Scholar
  3. B. Cook, A. Podelski, and A. Rybalchenko. Proving thread termination. In PLDI, pages 320-330. ACM, 2007. Google Scholar
  4. B. Cook, A. Podelski, and A. Rybalchenko. Proving program termination. Commun. ACM, 54(5), 2011. Google Scholar
  5. M. Dezani-Ciancaglini, D. Mostrous, N. Yoshida, and S. Drossopoulou. Session types for object-oriented languages. In D. Thomas, editor, ECOOP, volume 4067 of LNCS, pages 328-352. Springer, 2006. Google Scholar
  6. P. Ganty and S. Genaim. Proving termination starting from the end. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of LNCS, pages 397-412. Springer, 2013. Google Scholar
  7. C. S. Gordon, M. D. Ernst, and D. Grossman. Static lock capabilities for deadlock freedom. In TLDI, pages 67-78. ACM, 2012. Google Scholar
  8. A. Gotsman, B. Cook, M. Parkinson, and V. Vafeiadis. Proving that non-blocking algorithms don't block. In POPL, pages 16-28. ACM, 2009. Google Scholar
  9. G. J. Holzmann. SPIN Model Checker, The: Primer and Reference Manual. Addison-Wesley Professional, 2003. Google Scholar
  10. N. Kobayashi. A new type system for deadlock-free processes. In C. Baier and H. Hermanns, editors, CONCUR, volume 4137 of LNCS, pages 233-247. Springer, 2006. Google Scholar
  11. D.-K. Le, W.-N. Chin, and Y.-M. Teo. An expressive framework for verifying deadlock freedom. In D. Van Hung and M. Ogawa, editors, ATVA, volume 8172 of LNCS, pages 287-302. Springer, 2013. Google Scholar
  12. T. C. Le, C. Gherghina, A. Hobor, and W.-N. Chin. A resource-based logic for termination and non-termination proofs. In S. Merz and J. Pang, editors, ICFEM, volume 8829 of LNCS, pages 267-283. Springer, 2014. Google Scholar
  13. K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In E. M. Clarke and A. Voronkov, editors, LPAR, volume 6355 of LNCS, pages 348-370. Springer, 2010. Google Scholar
  14. K. R. M. Leino and P. Müller. A basis for verifying multi-threaded programs. In G. Castagna, editor, ESOP, volume 5502 of LNCS, pages 378-393. Springer, 2009. Google Scholar
  15. K. R. M. Leino, P. Müller, and J. Smans. Deadlock-free channels and locks. In A. D. Gordon, editor, ESOP, volume 6012 of LNCS, pages 407-426. Springer, 2010. Google Scholar
  16. Z. Manna and A. Pnueli. A hierarchy of temporal properties. In C. Dwork, editor, PODC, pages 377-410. ACM, 1990. Google Scholar
  17. Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 83(1):97–130, 1991. Google Scholar
  18. Z. Manna and A. Pnueli. Verification of parameterized programs. Specification and Validation Methods, pages 167-230, 1995. Google Scholar
  19. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446-455. ACM, 2007. Google Scholar
  20. M. J. Parkinson and G. Bierman. Separation logic and abstraction. In POPL, pages 247-258. ACM, 2005. Google Scholar
  21. M. J. Parkinson and A. J. Summers. The relationship between separation logic and implicit dynamic frames. In G. Barthe, editor, ESOP, volume 6602 of LNCS, pages 439-458. Springer, 2011. Google Scholar
  22. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55-74. IEEE Computer Society Press, 2002. Google Scholar
  23. J. Smans, B. Jacobs, and F. Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In S. Drossopoulou, editor, ECOOP, volume 5653 of LNCS, pages 148-172. Springer, 2009. Google Scholar
  24. K. Suenaga. Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references. In G. Ramalingam, editor, APLAS, volume 5356 of LNCS, pages 155-170. Springer, 2008. 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