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

research-article

Open access

Layered and object-based game semantics

Authors:

Arthur Oliveira Vale,

Paul-André Melliès,

Jérémie Koenig,

Léo StefanescoAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 6, Issue POPL

Article No.: 42, Pages 1 - 32

https://doi.org/10.1145/3498703

Published: 12 January 2022 Publication History

Abstract

Large-scale software verification relies critically on the use of compositional languages, semantic models, specifications, and verification techniques. Recent work on certified abstraction layers synthesizes game semantics, the refinement calculus, and algebraic effects to enable the composition of heterogeneous components into larger certified systems. However, in existing models of certified abstraction layers, compositionality is restricted by the lack of encapsulation of state.

In this paper, we present a novel game model for certified abstraction layers where the semantics of layer interfaces and implementations are defined solely based on their observable behaviors. Our key idea is to leverage Reddy's pioneer work on modeling the semantics of imperative languages not as functions on global states but as objects with their observable behaviors. We show that a layer interface can be modeled as an object type (i.e., a layer signature) plus an object strategy. A layer implementation is then essentially a regular map, in the sense of Reddy, from an object with the underlay signature to that with the overlay signature. A layer implementation is certified when its composition with the underlay object strategy implements the overlay object strategy. We also describe an extension that allows for non-determinism in layer interfaces.

After formulating layer implementations as regular maps between object spaces, we move to concurrency and design a notion of concurrent object space, where sequential traces may be identified modulo permutation of independent operations. We show how to express protected shared object concurrency, and a ticket lock implementation, in a simple model based on regular maps between concurrent object spaces.

Supplementary Material

Auxiliary Presentation Video (popl22main-p327-p-video.mp4)

This is a summary of a POPL 2022 presentation on "Layered and Object-Based Game Semantics".

Download
32.96 MB

References

[1]

2015-2021. DeepSpec: The Science of Deep Specifications. https://deepspec.org/

[2]

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for PCF. Inf. Comput., 163, 2 (2000), 409–470. issn:0890-5401 https://doi.org/10.1006/inco.2000.2930

Digital Library

[3]

Samson Abramsky and Guy McCusker. 1997. Linearity, Sharing and State: A Fully Abstract Game Semantics for Idealized Algol with Active Expressions. Birkhäuser Boston, Boston, MA. 297–329. isbn:978-1-4757-3851-3 https://doi.org/10.1007/978-1-4757-3851-3_10

[4]

Samson Abramsky and Guy McCusker. 1999. Game Semantics. In Computational Logic, Ulrich Berger and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1–55. isbn:978-3-642-58622-4

[5]

Andrew W. Appel. 2011. Verified Software Toolchain. In Proceedings of the 20th European Symposium on Programming (ESOP 2011). Springer, Berlin, Heidelberg. 1–17. isbn:978-3-642-19717-8 https://doi.org/10.1007/978-3-642-19718-5_1

[6]

Andrew W Appel, Lennart Beringer, Adam Chlipala, Benjamin C Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. 2017. Position Paper: The Science of Deep Specification. Phil. Trans. R. Soc. A, 375, 2104 (2017), 20160331. https://doi.org/10.1098/rsta.2016.0331

[7]

Ralph-Johan Back and Joakim von Wright. 1998. Refinement Calculus: A Systematic Introduction. Springer, New York. isbn:978-1-4612-1674-2 https://doi.org/10.1007/978-1-4612-1674-2

[8]

Andreas Blass. 1992. A Game Semantics for Linear Logic. Ann. Pure Appl. Log., 56, 1–3 (1992), 183–220. issn:0168-0072 https://doi.org/10.1016/0168-0072(92)90073-9

[9]

Stephen Brookes. 2006. A Grainless Semantics for Parallel Programs with Shared Mutable Data. Electronic Notes in Theoretical Computer Science, 155 (2006), 277 – 307. issn:1571-0661 https://doi.org/10.1016/j.entcs.2005.11.060 Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI).

Digital Library

[10]

Stephen Brookes. 2007. A Semantics for Concurrent Separation Logic. Theoretical Computer Science, 375, 1 (2007), 227 – 270. issn:0304-3975 https://doi.org/10.1016/j.tcs.2006.12.034 Festschrift for John C. Reynolds’s 70th birthday.

Digital Library

[11]

Ana C. Calderon and Guy McCusker. 2010. Understanding Game Semantics Through Coherence Spaces. Electron. Notes Theor. Comput. Sci., 265 (2010), Sept., 231–244. issn:1571-0661 https://doi.org/10.1016/j.entcs.2010.08.014

Digital Library

[12]

Andrea Cerone, Alexey Gotsman, and Hongseok Yang. 2014. Parameterised Linearisability. In Automata, Languages, and Programming, Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 98–109. isbn:978-3-662-43951-7

[13]

Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. 2016. Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). Association for Computing Machinery, New York, NY, USA. 431–447. isbn:9781450342612 https://doi.org/10.1145/2908080.2908101

Digital Library

[14]

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare Logic for Certifying the FSCQ File System. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP ’15). Association for Computing Machinery, New York, NY, USA. 18–37. isbn:9781450338349 https://doi.org/10.1145/2815400.2815402

Digital Library

[15]

Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification. Proc. ACM Program. Lang., 1, ICFP (2017), Article 24, Aug., 30 pages. https://doi.org/10.1145/3110268

Digital Library

[16]

David Costanzo, Zhong Shao, and Ronghui Gu. 2016. End-to-End Verification of Information-Flow Security for C and Assembly Programs. SIGPLAN Not., 51, 6 (2016), June, 648–664. issn:0362-1340 https://doi.org/10.1145/2980983.2908100

Digital Library

[17]

Ivana Filipović, Peter O’Hearn, Noam Rinetzky, and Hongseok Yang. 2009. Abstraction for Concurrent Objects. In Programming Languages and Systems, Giuseppe Castagna (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 252–266. isbn:978-3-642-00590-9

[18]

Dan R. Ghica and Andrzej S. Murawski. 2008. Angelic Semantics of Fine-Grained Concurrency. Annals of Pure and Applied Logic, 151, 2 (2008), 89 – 114. issn:0168-0072 https://doi.org/10.1016/j.apal.2007.10.005

[19]

Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science, 50, 1 (1987), 1–101. issn:0304-3975 https://doi.org/10.1016/0304-3975(87)90045-4

Digital Library

[20]

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). Association for Computing Machinery, New York, NY, USA. 595–608. isbn:9781450333009 https://doi.org/10.1145/2676726.2676975

Digital Library

[21]

Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, and David Costanzo. 2019. Building Certified Concurrent OS Kernels. Commun. ACM, 62, 10 (2019), Sept., 89–99. issn:0001-0782 https://doi.org/10.1145/3356903

Digital Library

[22]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI’16). USENIX Association, USA. 653–669. isbn:9781931971331

Digital Library

[23]

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified Concurrent Abstraction Layers. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). Association for Computing Machinery, New York, NY, USA. 646–661. isbn:9781450356985 https://doi.org/10.1145/3192366.3192381

Digital Library

[24]

Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst., 12, 3 (1990), July, 463–492. issn:0164-0925 https://doi.org/10.1145/78969.78972

Digital Library

[25]

J. M. E. Hyland and C.-H. L. Ong. 2000. On Full Abstraction for PCF: I, II, and III. Inf. Comput., 163, 2 (2000), 285–408. https://doi.org/10.1006/inco.2000.2917

Digital Library

[26]

A. Kock. 1972. Strong functors and monoidal monads. Archiv der Mathematik, 23 (1972), 113–120.

[27]

Jérémie Koenig. 2021. Grounding Game Semantics in Categorical Algebra. In Proceedings of the Fourth International Conference on Applied Category Theory, Kohei Kishida (Ed.) (ACT 2021). To appear.

[28]

Jérémie Koenig and Zhong Shao. 2020. Refinement-Based Game Semantics for Certified Abstraction Layers. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’20). Association for Computing Machinery, New York, NY, USA. 633–647. isbn:9781450371049 https://doi.org/10.1145/3373718.3394799

Digital Library

[29]

Jérémie Koenig and Zhong Shao. 2021. CompCertO: Compiling Certified Open C Components. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Association for Computing Machinery, New York, NY, USA. 1095–1109. isbn:9781450383912 https://doi.org/10.1145/3453483.3454097

Digital Library

[30]

Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM, 52, 7 (2009), July, 107–115. issn:0001-0782 https://doi.org/10.1145/1538788.1538814

Digital Library

[31]

Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon. 2019. Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation. Proc. ACM Program. Lang., 4, POPL (2019), Article 20, Dec., 31 pages. https://doi.org/10.1145/3371088

Digital Library

[32]

Antoni W. Mazurkiewicz. 1995. Introduction to Trace Theory. In The Book of Traces, Volker Diekert and Grzegorz Rozenberg (Eds.). World Scientific, 3–41. https://doi.org/10.1142/9789814261456_0001

[33]

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 ’18). Association for Computing Machinery, New York, NY, USA. 699–708. isbn:9781450355834 https://doi.org/10.1145/3209108.3209116

Digital Library

[34]

Paul-André Melliès and Léo Stefanesco. 2020. Concurrent Separation Logic Meets Template Games. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’20). Association for Computing Machinery, New York, NY, USA. 742–755. isbn:9781450371049 https://doi.org/10.1145/3373718.3394762

Digital Library

[35]

Paul-André Melliès and Noam Zeilberger. 2015. Functors Are Type Refinement Systems. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). Association for Computing Machinery, New York, NY, USA. 3–16. isbn:9781450333009 https://doi.org/10.1145/2676726.2676970

Digital Library

[36]

Paul-André Melliès. 2009. Categorical Semantics of Linear Logic. In Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses 27. Société Mathématique de France, Paris, France. 1–196.

[37]

Andrzej S. Murawski and Nikos Tzevelekos. 2014. Game Semantics for Interface Middleweight Java. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA. 517–528. isbn:9781450325448 https://doi.org/10.1145/2535838.2535880

Digital Library

[38]

Andrzej S. Murawski and Nikos Tzevelekos. 2019. Higher-order Linearisability. Journal of Logical and Algebraic Methods in Programming, 104 (2019), 86–116. issn:2352-2208 https://doi.org/10.1016/j.jlamp.2019.01.002

[39]

Peter W. O’Hearn. 2004. Resources, Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 49–67. isbn:978-3-540-28644-8

[40]

Peter W. O’Hearn and Uday S. Reddy. 1999. Objects, interference, and the Yoneda embedding. Theoretical Computer Science, 228, 1 (1999), 253–282. issn:0304-3975 https://doi.org/10.1016/S0304-3975(98)00360-0

Digital Library

[41]

Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco. 2021. Layered and Object-Based Game Semantics. Yale Univ. https://flint.cs.yale.edu/publications/layered.html

[42]

Gordon Plotkin and John Power. 2001. Adequacy for Algebraic Effects. In Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2001). Springer, Berlin, Heidelberg. 1–24. isbn:978-3-540-45315-4 https://doi.org/10.1007/3-540-45315-6_1

[43]

Gordon Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In Proceedings of the 18th European Symposium on Programming (ESOP 2009). Springer, Berlin, Heidelberg. 80–94. https://doi.org/10.1007/978-3-642-00590-9_7

Digital Library

[44]

U.S. Reddy. 1994. Passivity and independence. In Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science. 342–352. https://doi.org/10.1109/LICS.1994.316055

[45]

Uday S. Reddy. 1993. A Linear Logic Model of State. Dept. of Computer Science, UIUC, Urbana, IL.

[46]

Uday S. Reddy. 1996. Global State Considered Unnecessary: An Introduction to Object-Based Semantics. LISP Symb. Comput., 9, 1 (1996), 7–76.

[47]

Uday S. Reddy. 2002. Objects and Classes in Algol-like Languages. Inf. Comput., 172, 1 (2002), Feb., 63–97. issn:0890-5401 https://doi.org/10.1006/inco.2001.2927

Digital Library

[48]

Uday S. Reddy. 2013. Automata-Theoretic Semantics of Idealized Algol with Passive Expressions. Electronic Notes in Theoretical Computer Science, 298 (2013), 325–348. issn:1571-0661 https://doi.org/10.1016/j.entcs.2013.09.020 Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIX.

Digital Library

[49]

Uday S. Reddy and Brian P. Dunphy. 2012. An Automata-Theoretic Model of Idealized Algol. In Automata, Languages, and Programming, Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 337–350. isbn:978-3-642-31585-5

[50]

Christian Retoré. 1997. Pomset logic: A non-commutative extension of classical linear logic. In Typed Lambda Calculi and Applications, Philippe de Groote and J. Roger Hindley (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 300–318. isbn:978-3-540-68438-1

[51]

Jerome H. Saltzer and M. Frans Kaashoek. 2009. Principles of Computer System Design. Morgan Kaufmann.

[52]

Zhong Shao. 2010. Certified Software. Commun. ACM, 53, 12 (2010), December, 56–66.

Digital Library

[53]

Vilhelm Sjöberg, Yuyang Sang, Shu-chun Weng, and Zhong Shao. 2019. DeepSEA: A Language for Certified System Software. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 136, Oct., 27 pages. issn:2475-1421 https://doi.org/10.1145/3360562

Digital Library

Cited By

Zhang YKoenig JShao ZWang Y(2025)Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement AlgebraProceedings of the ACM on Programming Languages10.1145/37049009:POPL(1903-1933)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704900
Oliveira Vale AWang ZChen YYou PShao Z(2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689792
Oliveira Vale AShao ZChen Y(2024)A Compositional Theory of LinearizabilityJournal of the ACM10.1145/364366871:2(1-107)Online publication date: 12-Apr-2024
https://dl.acm.org/doi/10.1145/3643668
Show More Cited By

Index Terms

Layered and object-based game semantics
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Linear logic
    2. Logic and verification
  2. Semantics and reasoning
    1. Program reasoning
    2. Program semantics

Recommendations

Refinement-Based Game Semantics for Certified Abstraction Layers
LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

Formal methods have advanced to the point where the functional correctness of various large system components has been mechanically verified. However, the diversity of semantic models used across projects makes it difficult to connect these component to ...
Software Model Checking Based on Game Semantics and CSP

We present an approach for software model checking based on game semantics and CSP. Open program fragments are compositionally modelled as CSP processes which represent their game semantics. This translation is performed by a prototype compiler. ...
Procedural implementation of algebraic specification

An implementation of an algebraic specification in an imperative programming language consists of a representation type, together with an invariant and an equivalence relation over it, and a procedure for each operator in the specification. A formal ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 6, Issue POPL

January 2022

1886 pages

EISSN:2475-1421

DOI:10.1145/3511309

Issue’s Table of Contents

Copyright © 2022 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2022

Published in PACMPL Volume 6, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

DARPA and NIWC Pacific
NSF

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
500
Total Downloads

Downloads (Last 12 months)162
Downloads (Last 6 weeks)21

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhang YKoenig JShao ZWang Y(2025)Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement AlgebraProceedings of the ACM on Programming Languages10.1145/37049009:POPL(1903-1933)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704900
Oliveira Vale AWang ZChen YYou PShao Z(2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689792
Oliveira Vale AShao ZChen Y(2024)A Compositional Theory of LinearizabilityJournal of the ACM10.1145/364366871:2(1-107)Online publication date: 12-Apr-2024
https://dl.acm.org/doi/10.1145/3643668
Chappe NHe PHenrio LZakowski YZdancewic S(2023)Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in CoqProceedings of the ACM on Programming Languages10.1145/35712547:POPL(1770-1800)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571254
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: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571231
Sammler MSpies SSong YD'Osualdo EKrebbers RGarg DDreyer D(2023)DimSum: A Decentralized Approach to Multi-language Semantics and VerificationProceedings of the ACM on Programming Languages10.1145/35712207:POPL(775-805)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571220

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents