Document Open Access Logo

Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning

Authors Cormac Flanagan , Stephen N. Freund

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.16.pdf
  • Filesize: 1.52 MB
  • 29 pages

Document Identifiers

Author Details

Cormac Flanagan
  • University of California, Santa Cruz, CA, USA
Stephen N. Freund
  • Williams College, Williamstown, MA, USA

Funding

This work was supported by NSF grants 2243636 and 2243637.

Cite AsGet BibTex

Cormac Flanagan and Stephen N. Freund. Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 16:1-16:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.16

Abstract

Rely-guarantee (RG) logic uses thread interference specifications (relies and guarantees) to reason about the correctness of multithreaded software. Unfortunately, RG logic requires each function postcondition to be "stabilized" or specialized to the behavior of other threads, making it difficult to write function specifications that are reusable at multiple call sites. This paper presents mover logic, which extends RG logic to address this problem via the notion of atomic functions. Atomic functions behave as if they execute serially without interference from concurrent threads, and so they can be assigned more general and reusable specifications that avoid the stabilization requirement of RG logic. Several practical verifiers (Calvin-R, QED, CIVL, Armada, Anchor, etc.) have demonstrated the modularity benefits of atomic function specifications. However, the complexity of these systems and their correctness proofs makes it challenging to understand and extend these systems. Mover logic formalizes the central ideas of reduction in a declarative program logic that provides a foundation for future work in this area.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Program specifications
  • Software and its engineering → Concurrent programming languages
  • Software and its engineering → Formal software verification
Keywords
  • concurrent program verification
  • reduction
  • rely-guarantee reasoning
  • synchronization

Metrics

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

Related Versions

References

  1. The Anchor verifier. Accessed: March 30, 2024. URL: http://www.anchor-verifier.com/.
  2. Anindya Banerjee, David A. Naumann, and Stan Rosenberg. Regional logic for local reasoning about global invariants. In ECOOP, volume 5142 of Lecture Notes in Computer Science, pages 387-411. Springer, 2008. Google Scholar
  3. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, volume 4111 of Lecture Notes in Computer Science, pages 115-137. Springer, 2005. Google Scholar
  4. Stefan Blom, Saeed Darabi, Marieke Huisman, and Wytse Oortwijn. The vercors tool set: Verification of parallel and concurrent software. In IFM, volume 10510 of Lecture Notes in Computer Science, pages 102-110. Springer, 2017. Google Scholar
  5. Stephen Brookes. A semantics for concurrent separation logic. Theor. Comput. Sci., 375(1-3):227-270, 2007. Google Scholar
  6. Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods Syst. Des., 50(2-3):97-139, 2017. Google Scholar
  7. Tej Chajed, M. Frans Kaashoek, Butler W. Lampson, and Nickolai Zeldovich. Verifying concurrent software using movers in CSPEC. In OSDI, pages 306-322. USENIX Association, 2018. Google Scholar
  8. A. T. Chamillard and Lori A. Clarke. Improving the accuracy of petri net-based analysis of concurrent programs. In ISSTA, pages 24-38. ACM, 1996. Google Scholar
  9. Qichang Chen, Liqiang Wang, Zijiang Yang, and Scott D. Stoller. HAVE: detecting atomicity violations via integrated dynamic and static analysis. In FASE, volume 5503 of Lecture Notes in Computer Science, pages 425-439. Springer, 2009. Google Scholar
  10. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer, 1981. Google Scholar
  11. Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8(2):244-263, 1986. Google Scholar
  12. The Coq proof assistant, 2023. URL: https://coq.inria.fr/.
  13. Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. Views: compositional reasoning for concurrent programs. In POPL, pages 287-300. ACM, 2013. Google Scholar
  14. Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis. Deny-guarantee reasoning. In ESOP, volume 5502 of Lecture Notes in Computer Science, pages 363-377. Springer, 2009. Google Scholar
  15. Tayfun Elmas. QED: a proof system based on reduction and abstraction for the static verification of concurrent software. In ICSE (2), pages 507-508. ACM, 2010. Google Scholar
  16. E. Allen Emerson and Edmund M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In ICALP, volume 85 of Lecture Notes in Computer Science, pages 169-181. Springer, 1980. Google Scholar
  17. Cormac Flanagan and Stephen N. Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In POPL, pages 256-267. ACM, 2004. Google Scholar
  18. Cormac Flanagan and Stephen N. Freund. Fasttrack: efficient and precise dynamic race detection. Commun. ACM, 53(11):93-101, 2010. Google Scholar
  19. Cormac Flanagan and Stephen N. Freund. The Anchor verifier for blocking and non-blocking concurrent software. Proc. ACM Program. Lang., 4(OOPSLA):156:1-156:29, 2020. Google Scholar
  20. Cormac Flanagan and Stephen N. Freund. Mover logic: A concurrent program logic for reduction and rely-guarantee reasoning (extended version), 2024. URL: https://arxiv.org/abs/2407.08070.
  21. Cormac Flanagan, Stephen N. Freund, Marina Lifshin, and Shaz Qadeer. Types for atomicity: Static checking and inference for java. ACM Trans. Program. Lang. Syst., 30(4):20:1-20:53, 2008. Google Scholar
  22. Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer. Exploiting purity for atomicity. In ISSTA, pages 221-231. ACM, 2004. Google Scholar
  23. Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. In PLDI, pages 338-349. ACM, 2003. Google Scholar
  24. Cormac Flanagan and Shaz Qadeer. Types for atomicity. In TLDI, pages 1-12. ACM, 2003. Google Scholar
  25. Stephen N. Freund and Shaz Qadeer. Checking concise specifications for multithreaded software. J. Object Technol., 3(6):81-101, 2004. Google Scholar
  26. Patrice Godefroid. Model checking for programming languages using verisoft. In POPL, pages 174-186. ACM Press, 1997. Google Scholar
  27. Patrice Godefroid and Pierre Wolper. A partial approach to model checking. In LICS, pages 406-415. IEEE Computer Society, 1991. Google Scholar
  28. Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. Certified concurrent abstraction layers. In PLDI, pages 646-661. ACM, 2018. Google Scholar
  29. John Hatcliff, Robby, and Matthew B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In VMCAI, volume 2937 of Lecture Notes in Computer Science, pages 175-190. Springer, 2004. Google Scholar
  30. Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran. Automated and modular refinement reasoning for concurrent programs. In CAV (2), volume 9207 of Lecture Notes in Computer Science, pages 449-465. Springer, 2015. Google Scholar
  31. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. Google Scholar
  32. 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. In NASA Formal Methods, volume 6617 of Lecture Notes in Computer Science, pages 41-55. Springer, 2011. Google Scholar
  33. Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596-619, 1983. Google Scholar
  34. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28:e20, 2018. Google Scholar
  35. Ioannis T. Kassios. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In FM, volume 4085 of Lecture Notes in Computer Science, pages 268-283. Springer, 2006. Google Scholar
  36. Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer. Inductive sequentialization of asynchronous programs. In PLDI, pages 227-242. ACM, 2020. Google Scholar
  37. Bernhard Kragl and Shaz Qadeer. Layered concurrent programs. In CAV (1), volume 10981 of Lecture Notes in Computer Science, pages 79-102. Springer, 2018. Google Scholar
  38. Bernhard Kragl and Shaz Qadeer. The civl verifier. In FMCAD, pages 143-152. IEEE, 2021. Google Scholar
  39. Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. Synchronizing the asynchronous. In CONCUR, volume 118 of LIPIcs, pages 21:1-21:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  40. Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. Refinement for structured concurrent programs. In CAV (1), volume 12224 of Lecture Notes in Computer Science, pages 275-298. Springer, 2020. Google Scholar
  41. Richard J. Lipton. Reduction: A method of proving properties of parallel programs. Commun. ACM, 18(12):717-721, 1975. Google Scholar
  42. Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao. Armada: low-effort verification of high-performance concurrent programs. In PLDI, pages 197-210. ACM, 2020. Google Scholar
  43. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In VMCAI, volume 9583 of Lecture Notes in Computer Science, pages 41-62. Springer, 2016. Google Scholar
  44. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Dependable Software Systems Engineering, volume 50 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 104-125. IOS Press, 2017. Google Scholar
  45. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gérard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In OSDI, pages 267-280. USENIX Association, 2008. Google Scholar
  46. Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271-307, 2007. Google Scholar
  47. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL, volume 2142 of Lecture Notes in Computer Science, pages 1-19. Springer, 2001. Google Scholar
  48. Doron A. Peled. Combining partial order reductions with on-the-fly model-checking. In CAV, volume 818 of Lecture Notes in Computer Science, pages 377-390. Springer, 1994. 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. Amit Sasturkar, Rahul Agarwal, Liqiang Wang, and Scott D. Stoller. Automated type-based analysis of data races and atomicity. In PPoPP, pages 83-94. ACM, 2005. Google Scholar
  51. Jan Smans, Bart Jacobs, Frank Piessens, and Wolfram Schulte. An automatic verifier for java-like programs based on dynamic frames. In FASE, volume 4961 of Lecture Notes in Computer Science, pages 261-275. Springer, 2008. Google Scholar
  52. Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, UK, 2008. Google Scholar
  53. Viktor Vafeiadis and Matthew J. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR, volume 4703 of Lecture Notes in Computer Science, pages 256-271. Springer, 2007. Google Scholar
  54. Liqiang Wang and Scott D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In PPoPP, pages 137-146. ACM, 2006. Google Scholar
  55. Liqiang Wang and Scott D. Stoller. Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng., 32(2):93-110, 2006. Google Scholar
  56. John Wickerson, Mike Dodds, and Matthew J. Parkinson. Explicit stabilisation for modular rely-guarantee reasoning. In ESOP, volume 6012 of Lecture Notes in Computer Science, pages 610-629. Springer, 2010. Google Scholar
  57. James R. Wilcox, Cormac Flanagan, and Stephen N. Freund. Verifiedft: a verified, high-performance precise dynamic race detector. In PPoPP, pages 354-367. ACM, 2018. Google Scholar
  58. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, 1994. Google Scholar
  59. Eran Yahav. Verifying safety properties of concurrent java programs using 3-valued logic. In POPL, pages 27-40. ACM, 2001. Google Scholar
  60. Jaeheon Yi, Tim Disney, Stephen N. Freund, and Cormac Flanagan. Cooperative types for controlling thread interference in java. In ISSTA, pages 232-242. ACM, 2012. Google Scholar
  61. Jaeheon Yi, Tim Disney, Stephen N. Freund, and Cormac Flanagan. Cooperative types for controlling thread interference in java. Sci. Comput. Program., 112:227-260, 2015. Google Scholar
  62. Jaeheon Yi and Cormac Flanagan. Effects for cooperable and serializable threads. In TLDI, pages 3-14. ACM, 2010. 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