Document Open Access Logo

A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras

Authors Vincent Jackson , Toby Murray , Christine Rizkallah

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.23.pdf
  • Filesize: 0.76 MB
  • 16 pages

Document Identifiers

Author Details

Vincent Jackson
  • The University of Melbourne, Australia
Toby Murray
  • The University of Melbourne, Australia
Christine Rizkallah
  • The University of Melbourne, Australia

Cite AsGet BibTex

Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.23

Abstract

This paper describes GenRGSep, an Isabelle/HOL library for the development of RGSep logics using a general algebraic state model. In particular, we develop an algebraic state models based on resource algebras that assume neither the presence of unit resources or the cancellativity law. If a new resource model is required, its components need only be proven an instance of a permission algebra, and then they can be composed together using tuples and functions. The proof of soundness is performed by Vafeiadis' operational soundness method. This method was originally formulated with respect to a concrete heap model. This paper adapts it to account for the absence of both units as well as the cancellativity law.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Concurrency
  • Theory of computation → Separation logic
Keywords
  • verification
  • concurrency
  • rely-guarantee
  • separation logic
  • resource algebras

Metrics

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

Supplementary Materials

References

  1. P Aczel. On an inference rule for parallel composition. Private communication to Cliff Jones, February 1983. URL: https://homepages.cs.ncl.ac.uk/cliff.jones/publications/MSs/PHGA-traces.pdf.
  2. Andrew W. Appel. Verified software toolchain. In Gilles Barthe, editor, Programming Languages and Systems, pages 1-17. Springer, Berlin, Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-19718-5_1.
  3. Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Chapter 6 - Separation algebras. In Program Logics for Certified Compilers. Cambridge University Press, 1 edition, April 2014. URL: https://doi.org/10.1017/CBO9781107256552.
  4. Katalin Bimbó, Jon Michael Dunn, and Nicholas Ferenz. Two manuscripts, one by Routley, one by Meyer: The origins of the Routley-Meyer semantics for relevance logics. The Australasian Journal of Logic, 15(2), 2018. URL: https://doi.org/10.26686/ajl.v15i2.4066.
  5. Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '05, page 259–270, New York, NY, USA, 2005. Association for Computing Machinery. URL: https://doi.org/10.1145/1040305.1040327.
  6. John Boyland. Checking interference with fractional permissions. In Radhia Cousot, editor, Static Analysis, pages 55-72. Springer, Berlin, Heidelberg, 2003. URL: https://doi.org/10.1007/3-540-44898-5_4.
  7. Stephen Brookes and Peter W. O'Hearn. Concurrent separation logic. ACM SIGLOG News, 3(3):47–65, aug 2016. URL: https://doi.org/10.1145/2984450.2984457.
  8. Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 366-378, 2007. URL: https://doi.org/10.1109/LICS.2007.30.
  9. Cristiano Calcagno, Matthew Parkinson, and Viktor Vafeiadis. Modular safety checking for fine-grained concurrency. In Hanne Riis Nielson and Gilberto Filé, editors, Static Analysis, pages 233-248. Springer, Berlin, Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-74061-2_15.
  10. Thibault Dardinier. Formalization of commcsl: A relational concurrent separation logic for proving information flow security in concurrent programs. Archive of Formal Proofs, March 2023. https://isa-afp.org/entries/CommCSL.html, Formal proof development.
  11. Edsger W. Dijkstra and Carel S. Scholten. Predicate calculus and program semantics. Springer-Verlag, Berlin, Heidelberg, 1990. URL: https://doi.org/10.1007/978-1-4612-3228-5.
  12. Robert Dockins, Aquinas Hobor, and Andrew W. Appel. A fresh look at separation algebras and share accounting. In Zhenjiang Hu, editor, Programming Languages and Systems, pages 161-177. Springer, Berlin, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-10672-9_13.
  13. Mike Dodds, Xinyu Feng, Matthew Parkinson, and Viktor Vafeiadis. Deny-guarantee reasoning. Technical Report UCAM-CL-TR-736, University of Cambridge, Computer Laboratory, January 2009. URL: https://doi.org/10.48456/tr-736.
  14. Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, and Lars Birkedal. Verifying custom synchronization constructs using higher-order separation logic. ACM Transactions on Programming Languages and Systems, 38(2), jan 2016. URL: https://doi.org/10.1145/2818638.
  15. Marco Eilers, Thibault Dardinier, and Peter Müller. CommCSL: Proving information flow security for concurrent programs using abstract commutativity. Proceedings of the ACM on Programming Languages, 7(PLDI), jun 2023. URL: https://doi.org/10.1145/3591289.
  16. Alexey Gotsman, Josh Berdine, and Byron Cook. Precision and the conjunction rule in concurrent separation logic. Electronic Notes in Theoretical Computer Science, 276:171-190, September 2011. URL: https://doi.org/10.1016/j.entcs.2011.09.021.
  17. Ian J. Hayes. Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects Computing, 28(6):1057-1078, 2016. URL: https://doi.org/10.1007/S00165-016-0384-0.
  18. C. A. R. Hoare. Procedures and parameters: an axiomatic approach. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages, pages 102-116. Springer, Berlin, Heidelberg, 1971. URL: https://doi.org/10.1007/BFb0059696.
  19. C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, aug 1978. URL: https://doi.org/10.1145/359576.359585.
  20. C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall International, 1985. URL: http://www.usingcsp.com/cspbook.pdf.
  21. C. A. R. Hoare. Procedures and parameters: an axiomatic approach. In Essays in Computing Science, chapter 6. Prentice-Hall, Inc., USA, 1989. URL: https://doi.org/10.5555/63445.C1104361.
  22. Vincent Jackson. General RGSep. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:e759950d2ebd7571c86913f8296dfb29aa24a108;origin=https://github.com/vjackson725/GeneralRGSep;visit=swh:1:snp:e72ee116f86e47757d405779e79638178e413d3a;anchor=swh:1:rev:f35714d61e01b378ec363cc3f5fd6f5965a54beb (visited on 2024-08-22). URL: https://github.com/vjackson725/GeneralRGSep/tree/itp24.
  23. C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596–619, oct 1983. URL: https://doi.org/10.1145/69575.69577.
  24. Cliff B. Jones. Development Methods for Computer Programs including a Notion of Interference. PhD thesis, Oxford University, June 1981. Printed as: Programming Research Group, Technical Monograph 25. URL: https://www.cs.ox.ac.uk/publications/publication3768-abstract.html.
  25. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  26. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. Mechanised separation algebra. In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, pages 332-337. Springer, Berlin, Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_22.
  27. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. Separation algebra. Archive of Formal Proofs, May 2012. https://isa-afp.org/entries/Separation_Algebra.html, Formal proof development.
  28. Robbert Krebbers. Separation algebras for C verification in Coq. In Dimitra Giannakopoulou and Daniel Kroening, editors, Verified Software: Theories, Tools and Experiments, pages 150-166. Springer, Cham, 2014. URL: https://doi.org/10.1007/978-3-319-12154-3_10.
  29. Peter Lammich. Refinement of parallel algorithms down to LLVM. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.24.
  30. Peter Lammich and Rene Meis. A separation logic framework for imperative HOL. Archive of Formal Proofs, November 2012. https://isa-afp.org/entries/Separation_Logic_Imperative_HOL.html, Formal proof development.
  31. Peter W. O’Hearn. Resources, concurrency, and local reasoning. Theoretical Computer Science, 375(1):271-307, 2007. Festschrift for John C. Reynolds’s 70th birthday. URL: https://doi.org/10.1016/j.tcs.2006.12.035.
  32. Richard Routley and Robert K. Meyer. The semantics of entailment. In Hugues Leblanc, editor, Truth, Syntax and Modality, volume 68 of Studies in Logic and the Foundations of Mathematics, pages 199-243. Elsevier, 1973. URL: https://doi.org/10.1016/S0049-237X(08)71541-6.
  33. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 28-32. Springer, Berlin, Heidelberg, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  34. The Coq Development Team. The Coq reference manual - release 8.19.1. https://coq.inria.fr/doc/V8.19.1/refman, 2024.
  35. Lawrence C. Paulson Tobias Nipkow, Markus Wenzel, editor. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  36. Thomas Tuerk. A formalisation of smallfoot in HOL. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 469-484. Springer, Berlin, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_32.
  37. Viktor Vafeiadis. Modular fine-grained concurrency verification. Technical Report UCAM-CL-TR-726, University of Cambridge, Computer Laboratory, July 2008. URL: https://doi.org/10.48456/tr-726.
  38. Viktor Vafeiadis. Concurrent separation logic and operational semantics. Electronic Notes in Theoretical Computer Science, 276:335-351, 2011. Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII). URL: https://doi.org/10.1016/j.entcs.2011.09.029.
  39. Viktor Vafeiadis and Matthew Parkinson. A marriage of rely/guarantee and separation logic. In Luís Caires and Vasco T. Vasconcelos, editors, CONCUR 2007 - Concurrency Theory, pages 256-271. Springer, Berlin, Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-74407-8_18.
  40. John Wickerson. Concurrent verification for sequential programs. Technical Report UCAM-CL-TR-834, University of Cambridge, Computer Laboratory, May 2013. URL: https://doi.org/10.48456/tr-834.
  41. John Wickerson, Mike Dodds, and Matthew Parkinson. Explicit stabilisation for modular rely-guarantee reasoning. In Andrew D. Gordon, editor, Programming Languages and Systems, pages 610-629. Springer, Berlin, Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-11957-6_32.
  42. Hongseok Yang and Peter O'Hearn. A semantic basis for local reasoning. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, pages 402-416. Springer, Berlin, Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-45931-6_28.
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