Document Open Access Logo

Transferring Obligations Through Synchronizations

Authors Jafar Hamin , Bart Jacobs

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.19.pdf
  • Filesize: 0.74 MB
  • 58 pages

Document Identifiers

Author Details

Jafar Hamin
  • imec-DistriNet, Department of Computer Science, KU Leuven, Belgium
Bart Jacobs
  • imec-DistriNet, Department of Computer Science, KU Leuven, Belgium

Funding

This research received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 731453 (project VESSEDIA), as well as Flemish Research Fund project grant G.0962.17N.

Acknowledgements

We thank three anonymous reviewers for their careful reading of our manuscript and their many insighful comments and suggestions, and also Amin Timany for his guidance on Coq.

Cite AsGet BibTex

Jafar Hamin and Bart Jacobs. Transferring Obligations Through Synchronizations. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 19:1-19:58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.19

Abstract

One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only performs the actions for which it has permissions and it also fulfills all of its obligations before it terminates. Although permissions can be transferred through synchronizations from a sender thread, where for example a message is sent or a condition variable is notified, to a receiver thread, where that message or that notification is received, in existing approaches obligations can only be transferred when a thread is forked. In this paper we introduce two mechanisms, one for channels and the other for condition variables, that allow obligations, along with permissions, to be transferred from the sender to the receiver, while ensuring that there is no state where the transferred obligations are lost, i.e. where they are discharged from the sender thread but not loaded onto the receiver thread yet. We show how these mechanisms can be used to modularly verify deadlock-freedom of a number of interesting programs, such as some variations of client-server programs, fair readers-writers locks, and dining philosophers, which cannot be modularly verified without such transfer. We also encoded the proposed separation logic-based proof rules in the VeriFast program verifier and succeeded in verifying the mentioned programs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
  • Software and its engineering → Deadlocks
  • Software and its engineering → Process synchronization
  • Software and its engineering → Formal software verification
  • Theory of computation → Hoare logic
Keywords
  • Hoare logic
  • separation logic
  • modular program verification
  • synchronization
  • transferring obligations
  • deadlock-freedom

Metrics

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

References

  1. Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal. Iron: Managing Obligations in Higher-Order Concurrent Separation Logic. To appear in POPL 2019: ACM SIGPLAN Symposium on Principles of Programming Languages, Lissabon, Portugal, 2019. Google Scholar
  2. Pontus Boström and Peter Müller. Modular verification of finite blocking in non-terminating programs, volume 37. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  3. John Boyland. Checking interference with fractional permissions. In International Static Analysis Symposium, pages 55-72. Springer, 2003. Google Scholar
  4. Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. Modular Termination Verification for Non-blocking Concurrency. In ESOP, pages 176-201, 2016. Google Scholar
  5. Ornela Dardha and Simon J Gay. A new linear logic for deadlock-free session-typed processes. In International Conference on Foundations of Software Science and Computation Structures, pages 91-109. Springer, 2018. Google Scholar
  6. Pedro de Carvalho Gomes, Dilian Gurov, and Marieke Huisman. Specification and Verification of Synchronization with Condition Variables. In International Workshop on Formal Techniques for Safety-Critical Systems, pages 3-19. Springer, 2016. Google Scholar
  7. Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. Session types for object-oriented languages. In European Conference on Object-Oriented Programming, pages 328-352. Springer, 2006. Google Scholar
  8. Xinyu Feng. Local rely-guarantee reasoning. In ACM SIGPLAN Notices, volume 44, pages 315-327. ACM, 2009. Google Scholar
  9. Pedro de C Gomes, Dilian Gurov, Marieke Huisman, and Cyrille Artho. Specification and verification of synchronization with condition variables. Science of Computer Programming, 163:174-189, 2018. Google Scholar
  10. Colin S Gordon, Michael D Ernst, and Dan Grossman. Static lock capabilities for deadlock freedom. In Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation, pages 67-78. ACM, 2012. Google Scholar
  11. Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local reasoning for storable locks and threads. In Asian Symposium on Programming Languages And Systems, pages 19-37. Springer, 2007. Google Scholar
  12. Christian Haack, Marieke Huisman, and Clément Hurlin. Reasoning about Java’s reentrant locks. In Asian Symposium on Programming Languages And Systems, pages 171-187. Springer, 2008. Google Scholar
  13. Christian Haack and Clément Hurlin. Separation logic contracts for a Java-like language with fork/join. In International Conference on Algebraic Methodology and Software Technology, pages 199-215. Springer, 2008. Google Scholar
  14. Jafar Hamin and Bart Jacobs. Modular verification of termination and execution time bounds using separation logic. In Information Reuse and Integration (IRI), 2016 IEEE 17th International Conference on, pages 110-117. IEEE, 2016. Google Scholar
  15. Jafar Hamin and Bart Jacobs. Deadlock-Free Monitors. In European Symposium on Programming, pages 415-441. Springer, 2018. Google Scholar
  16. Jafar Hamin and Bart Jacobs. Deadlock-free monitors: extended version. TR CW712, Department of Computer Science, KU Leuven, Belgium. Full version available at http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW712.abs.html, 2018. Google Scholar
  17. Jafar Hamin and Bart Jacobs. Deadlock-Free Monitors and Channels. Zenodo, http://doi.org/10.5281/zenodo.3241454, 2019. URL: http://dx.doi.org/10.5281/zenodo.3241454.
  18. Tony Hoare and Peter O'Hearn. Separation logic semantics for communicating processes. Electronic Notes in Theoretical Computer Science, 212:3-25, 2008. Google Scholar
  19. Aquinas Hobor, Andrew W Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic. In European Symposium on Programming, pages 353-367. Springer, 2008. Google Scholar
  20. Jan Hoffmann, Michael Marmar, and Zhong Shao. Quantitative reasoning for proving lock-freedom. In Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on, pages 124-133. IEEE, 2013. Google Scholar
  21. Bart Jacobs. Provably live exception handling. In Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, page 7. ACM, 2015. Google Scholar
  22. Bart Jacobs. VeriFast 18.02. Zenodo, http://doi.org/10.5281/zenodo.1182724, 2018. URL: http://dx.doi.org/10.5281/zenodo.1182724.
  23. Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. Modular termination verification. In LIPIcs-Leibniz International Proceedings in Informatics, volume 37. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  24. Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. Modular termination verification of single-threaded and multithreaded programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 40(3):12, 2018. Google Scholar
  25. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. NASA Formal Methods, 6617:41-55, 2011. Google Scholar
  26. Bart Jacobs, Jan Smans, and Frank Piessens. A quick tour of the VeriFast program verifier. Programming Languages and Systems, pages 304-311, 2010. Google Scholar
  27. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. ACM SIGPLAN Notices, 50(1):637-650, 2015. Google Scholar
  28. Krishna M Kavi, Alireza Moshtaghi, and Deng-Jyi Chen. Modeling multithreaded applications using Petri nets. International Journal of Parallel Programming, 30(5):353-371, 2002. Google Scholar
  29. Naoki Kobayashi. A type system for lock-free processes. Information and Computation, 177(2):122-159, 2002. Google Scholar
  30. Naoki Kobayashi. A new type system for deadlock-free processes. In International Conference on Concurrency Theory, pages 233-247. Springer, 2006. Google Scholar
  31. Naoki Kobayashi and Cosimo Laneve. Deadlock analysis of unbounded process networks. Information and Computation, 252:48-70, 2017. Google Scholar
  32. Duy-Khanh Le, Wei-Ngan Chin, and Yong-Meng Teo. An expressive framework for verifying deadlock freedom. In International Symposium on Automated Technology for Verification and Analysis, pages 287-302. Springer, 2013. Google Scholar
  33. K Rustan M Leino, Peter Müller, and Jan Smans. Deadlock-free channels and locks. In European Symposium on Programming, pages 407-426. Springer, 2010. Google Scholar
  34. Hongjin Liang and Xinyu Feng. Progress of concurrent objects with partial methods. Proceedings of the ACM on Programming Languages, 2(POPL):20, 2017. Google Scholar
  35. Hongjin Liang, Xinyu Feng, and Zhong Shao. Compositional verification of termination-preserving refinement of concurrent programs. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), page 65. ACM, 2014. Google Scholar
  36. 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 Lecture Notes in Computer Science, pages 290-310. Springer, 2014. Google Scholar
  37. Peter W O’Hearn. Resources, concurrency, and local reasoning. Theoretical computer science, 375(1-3):271-307, 2007. Google Scholar
  38. Luca Padovani. Type-Based Analysis of Linear Communications. Behavioural Types: from Theory to Tools, page 193, 2017. Google Scholar
  39. Corneliu Popeea and Andrey Rybalchenko. Compositional Termination Proofs for Multi-threaded Programs. In TACAS, volume 12, pages 237-251. Springer, 2012. Google Scholar
  40. David Pym and Chris Tofts. A calculus and logic of resources and processes. Formal Aspects of Computing, 18(4):495-517, 2006. Google Scholar
  41. Azalea Raad, Jules Villard, and Philippa Gardner. Colosl: Concurrent local subjective logic. In European Symposium on Programming Languages and Systems, pages 710-735. Springer, 2015. Google Scholar
  42. John C Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on, pages 55-74. IEEE, 2002. Google Scholar
  43. Reuben NS Rowe and James Brotherston. Automatic cyclic termination proofs for recursive procedures in separation logic. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 53-65. ACM, 2017. Google Scholar
  44. Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames. In Proceedings of the 10th ECOOP Workshop on Formal Techniques for Java-like Programs, pages 1-12, 2008. Google Scholar
  45. Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In European Conference on Object-Oriented Programming, pages 148-172. Springer, 2009. Google Scholar
  46. Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames. ACM Transactions on Programming Languages and Systems (TOPLAS), 34(1):2, 2012. Google Scholar
  47. Kohei Suenaga. Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references. In Asian Symposium on Programming Languages and Systems, pages 155-170. Springer, 2008. Google Scholar
  48. Viktor Vafeiadis and Matthew Parkinson. A marriage of rely/guarantee and separation logic. In International Conference on Concurrency Theory, pages 256-271. Springer, 2007. Google Scholar
  49. Chao Wang and Kevin Hoang. Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability. In VMCAI, pages 376-394. Springer, 2014. 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 Imprint Privacy Contact