Document Open Access Logo

Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra

Authors Paul Brunet , David Pym

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.8.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Paul Brunet
  • University College London, UK
  • paul.brunet-zamansky.fr
David Pym
  • University College London, UK
  • www.cantab.net/users/david.pym/

Funding

This work has been supported by UK EPSRC Research Grant EP/R006865/1: Interface Reasoning for Interacting Systems (IRIS).

Acknowledgements

The authors are grateful to their colleagues at UCL and within IRIS project for their interest. We also thank the anonymous referees for their comments and suggestions.

Cite As Get BibTex

Paul Brunet and David Pym. Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.8

Abstract

Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protected from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themselves. This is often too restrictive for practical purposes. We provide a logic, "pomset logic", that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. In contrast with other approaches, this logic is not state-based, but rather characterizes the runtime behaviour of a program. We develop the basic metatheory for the relationship between pomset logic and CKA, including frame rules to support local reasoning, and illustrate this relationship with simple examples.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Separation logic
Keywords
  • Concurrent Kleene Algebra
  • Pomsets
  • Atomicity
  • Semantics
  • Separation
  • Local reasoning
  • Bunched logic
  • Frame rules

Metrics

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

Related Versions

Supplementary Materials

References

  1. Gabrielle Anderson and David Pym. A calculus and logic of bunched resources and processes. Theor. Comp. Sci., 614, 2016. URL: https://doi.org/10.1016/j.tcs.2015.11.035.
  2. Johan Van Benthem. Logical Dynamics of Information and Interaction. Cambridge University Press, 2014. Google Scholar
  3. Stephen Brookes and Peter W. O'Hearn. Concurrent Separation Logic. ACM SIGLOG News, 3(3), August 2016. URL: https://doi.org/10.1145/2984450.2984457.
  4. Paul Brunet, Damien Pous, and Georg Struth. On Decidability of Concurrent Kleene Algebra. In CONCUR, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.28.
  5. Matthew Collinson and David Pym. Algebra and Logic for Resource-Based Systems Modelling. Math. Str. Comp. Sci., 19(5), 2009. URL: https://doi.org/10.1017/S0960129509990077.
  6. Amina Doumane, Denis Kuperberg, Damien Pous, and Pierre Pradic. Kleene Algebra with Hypotheses. In FoSSaCS, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_12.
  7. Didier Galmiche, Daniel Méry, and David Pym. The Semantics of BI and Resource Tableaux. Math. Str. Comp. Sci., 15(6), December 2005. URL: https://doi.org/10.1017/S0960129505004858.
  8. Jay L. Gischer. The Equational Theory of Pomsets. Theor. Comp. Sci., 61(2-3), 1988. URL: https://doi.org/10.1016/0304-3975(88)90124-7.
  9. Jan Grabowski. On partial languages. Fund. Math., 4(2), 1981. Google Scholar
  10. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In ICALP, 1980. URL: https://doi.org/10.1007/3-540-10003-2_79.
  11. C.A.R. Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene Algebra. In CONCUR, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_27.
  12. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an Assertion Language for Mutable Data Structures. In POPL, 2001. URL: https://doi.org/10.1145/373243.375719.
  13. Lalita Jategaonkar and Albert R. Meyer. Deciding true concurrency equivalences on safe, finite nets. Theor. Comp. Sci., 154(1), 1996. URL: https://doi.org/10.1016/0304-3975(95)00132-8.
  14. Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness. In FoSSaCS, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_20.
  15. Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi. Concurrent Kleene Algebra: Free Model and Completeness. In ESOP, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_30.
  16. Casimir Kuratowski. Sur l'opération Ā de l'Analysis Situs. Fund. Math., 3(1), 1922. Google Scholar
  17. Michael R. Laurence and Georg Struth. Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages. In RAMiCS, 2014. URL: https://doi.org/10.1007/978-3-319-06251-8_5.
  18. Robin Milner. Communication and Concurrency. Prentice-Hall, Inc., 1989. Google Scholar
  19. Peter W. O'Hearn. Resources, Concurrency, and Local Reasoning. Theor. Comp. Sci., 375(1-3), May 2007. URL: https://doi.org/10.1016/j.tcs.2006.12.035.
  20. Peter W. O'Hearn, Rasmus L. Petersen, Jules Villard, and Akbar Hussain. On the Relation between Concurrent Separation Logic and Concurrent Kleene Algebra. J. Log. Algebr. Methods Program., 84(3), May 2015. URL: https://doi.org/10.1016/j.jlamp.2014.08.002.
  21. Peter W. O'Hearn and David J. Pym. The Logic of Bunched Implications. Bull. Symb. Log., 5(2), 1999. URL: https://doi.org/10.2307/421090.
  22. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local Reasoning about Programs That Alter Data Structures. In CSL, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  23. David Pym. Resource Semantics: Logic as a Modelling Technology. ACM SIGLOG News, 6(2), April 2019. URL: https://doi.org/10.1145/3326938.3326940.
  24. Mohammad Raza and Philippa Gardner. Footprints in Local Reasoning. In FoSSaCS, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_15.
  25. Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In TLCA, 1997. URL: https://doi.org/10.1007/3-540-62688-3_43.
  26. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS, July 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  27. Jacobo Valdes, Robert E. Tarjan, and Eugene L. Lawler. The Recognition of Series Parallel Digraphs. SIAM J. Comput., 11(2), 1982. URL: https://doi.org/10.1137/0211023.
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