Document Open Access Logo

Towards Concurrent Quantitative Separation Logic

Authors Ira Fesefeldt , Joost-Pieter Katoen , Thomas Noll

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.25.pdf
  • Filesize: 0.89 MB
  • 24 pages

Document Identifiers

Author Details

Ira Fesefeldt
  • Software Modeling and Verification Group, RWTH Aachen University, Germany
Joost-Pieter Katoen
  • Software Modeling and Verification Group, RWTH Aachen University, Germany
Thomas Noll
  • Software Modeling and Verification Group, RWTH Aachen University, Germany

Cite AsGet BibTex

Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll. Towards Concurrent Quantitative Separation Logic. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.25

Abstract

In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combine two kinds of separation logic - Quantitative Separation Logic and Concurrent Separation Logic - into a new separation logic that enables reasoning about lower bounds of the probability to realise a postcondition by executing such a program.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Concurrent algorithms
  • Mathematics of computing → Probabilistic reasoning algorithms
Keywords
  • Randomization
  • Pointers
  • Heap-Manipulating
  • Separation Logic
  • Concurrency

Metrics

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

Related Versions

References

  1. Christel Baier, Frank Ciesinski, and Markus Grosser. PROBMELA: a modeling language for communicating probabilistic processes. In MEMOCODE, pages 57-66. IEEE, 2004. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  3. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Probabilistic relational Hoare logics for computer-aided security proofs. In MPC, pages 1-6. Springer, 2012. Google Scholar
  4. Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, and Thomas Noll. Foundations for entailment checking in quantitative separation logic. In ESOP, pages 57-84. Springer, 2022. Google Scholar
  5. Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang., 3(POPL):34:1-34:29, 2019. Google Scholar
  6. Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. In CAV, pages 178-192. Springer, 2007. Google Scholar
  7. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, pages 115-137. Springer, 2005. Google Scholar
  8. Burton H. Bloom. Space/time trade-offs in hash coding with allowable errors. Commun. ACM, 13(7):422-426, 1970. Google Scholar
  9. Stephen Brookes and Peter W. O'Hearn. Concurrent separation logic. ACM SIGLOG News, 3(3):47-65, 2016. Google Scholar
  10. Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6):26:1-26:66, 2011. Google Scholar
  11. Michael Carbin, Sasa Misailovic, and Martin C. Rinard. Verifying quantitative reliability for programs that execute on unreliable hardware. Commun. ACM, 59(8):83-91, 2016. Google Scholar
  12. Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. Google Scholar
  13. Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang. Views: Compositional reasoning for concurrent programs. In POPL, pages 287-300. ACM, 2013. Google Scholar
  14. Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. Concurrent abstract predicates. In ECOOP, pages 504-528. Springer, 2010. Google Scholar
  15. Emanuele D’Osualdo, Julian Sutherland, Azadeh Farzan, and Philippa Gardner. TaDA live: Compositional reasoning for termination of fine-grained concurrent programs. ACM Trans. Program. Lang. Syst., 43(4), 2021. Google Scholar
  16. Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll. Towards concurrent quantitative separation logic. CoRR, abs/2207.02822, 2022. Google Scholar
  17. Keir Fraser. Practical lock-freedom. Technical Report UCAM-CL-TR-579, University of Cambridge, Computer Laboratory, 2004. Google Scholar
  18. Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. Reasoning about optimistic concurrency using a program logic for history. In CONCUR, pages 388-402. Springer, 2010. Google Scholar
  19. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Probabilistic programming. In FOSE, pages 167-181. ACM, 2014. Google Scholar
  20. Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv. Thread-modular shape analysis. In PLDI, pages 266-277. ACM, 2007. Google Scholar
  21. Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Performance Evaluation, 73:110-132, 2014. Google Scholar
  22. Sergiu Hart and Micha Sharir. Concurrent probabilistic programs, or: How to schedule if you must. SIAM J. Comput., 14(4):991-1012, 1985. Google Scholar
  23. Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent programs. ACM Trans. Program. Lang. Syst., 5(3):356-380, 1983. Google Scholar
  24. Max P. L. Haslbeck. Verified Quantitative Analysis of Imperative Algorithms. PhD thesis, Technical University of Munich, Germany, 2021. Google Scholar
  25. Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. Modular verification for almost-sure termination of probabilistic programs. Proc. ACM Program. Lang., 3(OOPSLA):129:1-129:29, 2019. Google Scholar
  26. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In POPL, pages 14-26. ACM, 2001. Google Scholar
  27. Kenneth E. Iverson. A Programming Language. John Wiley & Sons, Inc., USA, 1962. Google Scholar
  28. 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 NFM, pages 41-55. Springer, 2011. Google Scholar
  29. Claire Jones. Probabilistic Non-Determinism. PhD thesis, University of Edinburgh, 1992. Google Scholar
  30. Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596-619, 1983. Google Scholar
  31. 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
  32. 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. In POPL, pages 637-650. ACM, 2015. Google Scholar
  33. Benjamin L. Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM, 65(5), 2018. Google Scholar
  34. Dexter Kozen. Semantics of probabilistic programs. In FOCS, pages 101-114. IEEE Computer Society, 1979. Google Scholar
  35. Dexter Kozen. A probabilistic PDL. In STOC, pages 291-297. ACM, 1983. Google Scholar
  36. Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, and Philipp Rümmer. Fair termination for parameterized probabilistic concurrent systems. In TACAS, pages 499-517. Springer, 2017. Google Scholar
  37. Christoph Matheja. Automated Reasoning and Randomization in Separation Logic. PhD thesis, RWTH Aachen University, Germany, 2020. Google Scholar
  38. Annabelle McIver and Carroll Morgan. Partial correctness for probabilistic demonic programs. Theoretical Computer Science, 266(1):513-541, 2001. Google Scholar
  39. Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. Google Scholar
  40. Annabelle McIver, Tahiry Rabehaja, and Georg Struth. Probabilistic rely-guarantee calculus. Theoretical Computer Science, 655:120-134, 2016. Google Scholar
  41. Michael Mitzenmacher and Eli Upfal. Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press, 2005. Google Scholar
  42. 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
  43. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. Communicating state transition systems for fine-grained concurrent resources. In ESOP, pages 290-310. Springer, 2014. Google Scholar
  44. Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. Bounded expectations: Resource analysis for probabilistic programs. SIGPLAN Not., 53(4):496-512, 2018. Google Scholar
  45. Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theoretical Computer Science, 375(1):271-307, 2007. Google Scholar
  46. Peter W. O'Hearn. Separation logic. Commun. ACM, 62(2):86-95, 2019. Google Scholar
  47. Ruzica Piskac, Thomas Wies, and Damien Zufferey. Automating separation logic using SMT. In CAV, pages 773-789. Springer, 2013. Google Scholar
  48. William Pugh. Skip lists: A probabilistic alternative to balanced trees. Commun. ACM, 33(6):668-676, 1990. Google Scholar
  49. Tobias Reinhard and Bart Jacobs. Ghost signals: Verifying termination of busy waiting. In CAV, pages 27-50. Springer, 2021. Google Scholar
  50. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55-74. IEEE Computer Society, 2002. Google Scholar
  51. Joseph Tassarotti and Robert Harper. A separation logic for concurrent randomized programs. Proc. ACM Program. Lang., 3(POPL):64:1-64:30, 2019. Google Scholar
  52. Michael L. Tiomkin. Probabilistic termination versus fair termination. Theor. Comput. Sci., 66(3):333-340, 1989. Google Scholar
  53. Viktor Vafeiadis. Concurrent separation logic and operational semantics. Electronic Notes in Theoretical Computer Science, 276:335-351, 2011. 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