More Web Proxy on the site http://driver.im/

research-article

Concurrent Separation Logic Meets Template Games

Authors:

Paul-André Melliès,

Léo StefanescoAuthors Info & Claims

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 742 - 755

https://doi.org/10.1145/3373718.3394762

Published: 08 July 2020 Publication History

Abstract

An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game semantics for higher-order programs, and Hoare logic for concurrent programs with shared memory and locks. We establish a deep and unexpected connection between two recent lines of work on concurrent separation logic (CSL) and on template game semantics for differential linear logic (DiLL). Thanks to this connection, we reformulate in the purely conceptual style of template games for DiLL the asynchronous and interactive interpretation of CSL designed by Melliès and Stefanesco in a recent work. We believe that the analysis reveals something important about the secret anatomy of CSL, and more specifically about the subtle interplay, of a categorical nature, between sequential composition, parallel product, errors and locks.

References

[1]

J. Baez and M. Stay. 2011. Physics, topology, logic and computation: A Rosetta Stone. Lecture Notes in Physics 813 (2011), 95--172.

[2]

Jean Bénabou. 1967. Introduction to bicategories. In Reports of the Midwest Category Seminar. Springer Berlin Heidelberg, Berlin, Heidelberg, 1--77.

[3]

F. Bonchi, B. König, and U. Montanari. 2006. Saturated Semantics for Reactive Systems. In 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06). 69--80.

[4]

Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. 2005. Permission Accounting in Separation Logic. In POPL.

[5]

Stephen Brookes. 2004. A semantics for concurrent separation logic. In CONCUR.

[6]

Brian Day and Ross Street. 1997. Monoidal Bicategories and Hopf Algebroids. Advances in Mathematics 129, 1 (1997), 99--157.

[7]

Brian Day and Ross Street. 2004. Quantum categories, star autonomy, and quantum groupoids. In Galois Theory, Hopf Algebras, and Semiabelian Categories. Fields Institute Communications, Vol. 43. American Mathematical Society, Providence, Rhode Island, 193--231.

[8]

Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views: compositional reasoning for concurrent programs. In POPL.

[9]

Clovis Eberhart, Tom Hirschowitz, and Alexis Laouar. 2019. Template Games, Simple Games, and Day Convolution. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany. 16:1--16:19.

[10]

Charles Ehresmann. 1963. Catégories structurées. Annales scientifiques de l'École Normale Supérieure 80, 4 (1963), 349--426.

[11]

Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raussen. 2016. Directed Algebraic Topology and Concurrency. Springer.

[12]

Marco Grandis. 2007. Collared cospans, cohomotopy and TQFT (cospans in algebraic topology, II). Theory Appl. Categ 18 (2007), 602--630.

[13]

Jonathan Hayman and Glynn Winskel. 2008. Independence and Concurrent Separation Logic. LMCS (2008).

[14]

Tony Hoare. 2013. Unifying Semantics for Concurrent Programming. In Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky - Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday. 139--149.

[15]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20.

[16]

Stephen Lack and Pawel Sobociński. 2004. Adhesive Categories. In Foundations of Software Science and Computation Structures, Igor Walukiewicz (Ed.). Springer Berlin Heidelberg, 273--288.

[17]

Paul-André Melliès. 2013. Dialogue Categories and Frobenius Monoids. In Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky - Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday, Bob Coecke, Luke Ong, and Prakash Panangaden (Eds.). Vol. 7860. Springer-Verlag.

[18]

Paul-André Melliès. 2019. Categorical Combinatorics of Scheduling and Synchronization in Game Semantics. Proc. ACM Program. Lang. 3, POPL, Article 23 (Jan. 2019), 30 pages.

Digital Library

[19]

Paul-André Melliès. 2019. Template games and differential linear logic. In LICS 2019.

[20]

Paul-André Melliès and Léo Stefanesco. 2017. A Game Semantics for Concurrent Separation Logic. In MFPS.

[21]

Paul-André Melliès and Léo Stefanesco. 2018. An Asynchronous Soundness Theorem for Concurrent Separation Logic. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018.

Digital Library

[22]

Paul-André Melliès and Léo Stefanesco. 2020. Concurrent Separation Logic Meets Template Games. TODO (2020).

[23]

Jeffrey Morton. 2006. Double Bicategories and Double Cospans. Journal of Homotopy and Related Structures 4(11 2006).

[24]

V. Sassone and P. Sobociński. 2005. Reactive Systems over Cospans. In Logic in Computer Science, LiCS '05. IEEE Press, 311--320.

[25]

V. Sassone and P. Sobocinski. 2005. Reactive systems over cospans. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05). 311--320.

[26]

Viktor Vafeiadis. 2011. Concurrent Separation Logic and Operational Semantics. ENTCS 276 (2011).

[27]

Rob J. van Glabbeek. 2006. On the expressiveness of higher dimensional automata. Theoretical Computer Science 356, 3 (2006).

Cited By

Oliveira Vale AShao ZChen Y(2024)A Compositional Theory of LinearizabilityJournal of the ACM10.1145/364366871:2(1-107)Online publication date: 27-Jan-2024
https://dl.acm.org/doi/10.1145/3643668
Oliveira Vale AShao ZChen Y(2023)A Compositional Theory of LinearizabilityProceedings of the ACM on Programming Languages10.1145/35712317:POPL(1089-1120)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571231
Behr NHarmer RKrivine J(2023)Fundamentals of Compositional Rewriting TheoryJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100893(100893)Online publication date: Jul-2023
https://doi.org/10.1016/j.jlamp.2023.100893
Show More Cited By

Index Terms

Concurrent Separation Logic Meets Template Games
1. Theory of computation

Recommendations

An Asynchronous Soundness Theorem for Concurrent Separation Logic
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every ...
Interactive proofs in higher-order concurrent separation logic
POPL '17

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

July 2020

986 pages

ISBN:9781450371049

DOI:10.1145/3373718

Conference Chairs:
Holger Hermanns,
Lijun Zhang,
Naoki Kobayashi,
General Chair:
Dale Miller

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 July 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

LICS '20

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science

July 8 - 11, 2020

Saarbrücken, Germany

Acceptance Rates

LICS '20 Paper Acceptance Rate 69 of 174 submissions, 40%;

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
66
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)3

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Oliveira Vale AShao ZChen Y(2024)A Compositional Theory of LinearizabilityJournal of the ACM10.1145/364366871:2(1-107)Online publication date: 27-Jan-2024
https://dl.acm.org/doi/10.1145/3643668
Oliveira Vale AShao ZChen Y(2023)A Compositional Theory of LinearizabilityProceedings of the ACM on Programming Languages10.1145/35712317:POPL(1089-1120)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571231
Behr NHarmer RKrivine J(2023)Fundamentals of Compositional Rewriting TheoryJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100893(100893)Online publication date: Jul-2023
https://doi.org/10.1016/j.jlamp.2023.100893
Oliveira Vale AMelliès PShao ZKoenig JStefanesco L(2022)Layered and object-based game semanticsProceedings of the ACM on Programming Languages10.1145/34987036:POPL(1-32)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498703

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents