[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

DimSum: A Decentralized Approach to Multi-language Semantics and Verification

Published: 11 January 2023 Publication History

Abstract

Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g. fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this paper, we explore the problem of how to avoid such global restrictions.
Concretely, we present DimSum: a new, decentralized approach to multi-language semantics and verification, which we have implemented in the Coq proof assistant. Decentralization means that we can define and reason about languages independently from each other (as independent modules communicating via events), but also combine and translate between them when necessary (via a library of combinators).
We apply DimSum to a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec. We evaluate DimSum on two case studies: an Asm library extending Rec with support for pointer comparison, and a coroutine library for Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications, despite the behavior of the Asm libraries not being syntactically expressible in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm, showing that it is compatible with these Asm libraries.

References

[1]
Martín Abadi and Gordon D. Plotkin. 2010. On Protection by Layout Randomization. In CSF. IEEE Computer Society, 337–351. https://doi.org/10.1109/CSF.2010.30
[2]
Amal Ahmed and Matthias Blume. 2011. An equivalence-preserving CPS translation via multi-language semantics. In ICFP. ACM, 431–444. https://doi.org/10.1145/2034773.2034830
[3]
Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. 1998. Alternating Refinement Relations. In CONCUR (LNCS, Vol. 1466). Springer, 163–178. https://doi.org/10.1007/BFb0055622
[4]
Nick Benton and Chung-Kil Hur. 2009. Biorthogonality, step-indexing and compiler correctness. In ICFP. ACM, 97–108. https://doi.org/10.1145/1596550.1596567
[5]
Nick Benton and Chung-Kil Hur. 2010. Realizability and compositional compiler correctness for a polymorphic language. Microsoft Research. https://sf.snu.ac.kr/publications/cccmsrtr.pdf
[6]
Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel. 2014. Verified Compilation for Shared-Memory C. In ESOP (LNCS, Vol. 8410). Springer, 107–127. https://doi.org/10.1007/978-3-642-54833-8_7
[7]
Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. 1981. Alternation. J. ACM, 28, 1 (1981), 114–133. https://doi.org/10.1145/322234.322243
[8]
Robert W. Floyd. 1967. Nondeterministic Algorithms. J. ACM, 14, 4 (1967), 636–644. https://doi.org/10.1145/321420.321422
[9]
Carsten Fritz and Thomas Wilke. 2005. Simulation relations for alternating Büchi automata. Theor. Comput. Sci., 338, 1-3 (2005), 275–314. https://doi.org/10.1016/j.tcs.2005.01.016
[10]
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. 2022. Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang., 6, POPL (2022), 1–31. https://doi.org/10.1145/3498689
[11]
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 POPL. ACM, 595–608. https://doi.org/10.1145/2676726.2676975
[12]
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 PLDI. ACM, 646–661. https://doi.org/10.1145/3192366.3192381
[13]
C. A. R. Hoare. 1978. Communicating Sequential Processes. Commun. ACM, 21, 8 (1978), 666–677. https://doi.org/10.1145/359576.359585
[14]
Chung-Kil Hur and Derek Dreyer. 2011. A Kripke logical relation between ML and assembly. In POPL. ACM, 133–146. https://doi.org/10.1145/1926385.1926402
[15]
Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. 2012. The marriage of bisimulations and Kripke logical relations. In POPL. ACM, 59–72. https://doi.org/10.1145/2103656.2103666
[16]
Alan Jeffrey and Julian Rathke. 2005. Java Jr: Fully Abstract Trace Semantics for a Core Java Language. In ESOP (Lecture Notes in Computer Science, Vol. 3444). Springer, 423–438. https://doi.org/10.1007/978-3-540-31987-0_29
[17]
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. https://doi.org/10.1017/S0956796818000151
[18]
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. ACM, 637–650. https://doi.org/10.1145/2676726.2676980
[19]
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2016. Lightweight verification of separate compilation. In POPL. ACM, 178–190. https://doi.org/10.1145/2837614.2837642
[20]
Jérémie Koenig and Zhong Shao. 2021. CompCertO: compiling certified open C components. In PLDI. ACM, 1095–1109. https://doi.org/10.1145/3453483.3454097
[21]
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. MoSeL: A general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang., 2, ICFP (2018), 77:1–77:30. https://doi.org/10.1145/3236772
[22]
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP (LNCS, Vol. 10201). Springer, 696–723. https://doi.org/10.1007/978-3-662-54434-1_26
[23]
Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. ACM, 205–217. https://doi.org/10.1145/3009837.3009855
[24]
James Laird. 2007. A Fully Abstract Trace Semantics for General References. In ICALP (LNCS, Vol. 4596). Springer, 667–679. https://doi.org/10.1007/978-3-540-73420-8_58
[25]
Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL. ACM, 42–54. https://doi.org/10.1145/1111037.1111042
[26]
Xavier Leroy and Sandrine Blazy. 2008. Formal verification of a C-like memory model and its uses for verifying program transformations. JAR, 41, 1 (2008), 1–31. https://doi.org/10.1007/s10817-008-9099-0
[27]
Phillip Mates, Jamie Perconti, and Amal Ahmed. 2019. Under Control: Compositionally Correct Closure Conversion with Mutable State. In PPDP. ACM, 16:1–16:15. https://doi.org/10.1145/3354166.3354181
[28]
Jacob Matthews and Robert Bruce Findler. 2007. Operational semantics for multi-language programs. In POPL. ACM, 3–10. https://doi.org/10.1145/1190216.1190220
[29]
Robin Milner. 1999. Communicating and Mobile Systems: the π -Calculus. Cambridge University Press. isbn:978-0-521-65869-0
[30]
Robin Milner, Joachim Parrow, and David Walker. 1992. A Calculus of Mobile Processes, I/II. Inf. Comput., 100, 1 (1992), 1–40. https://doi.org/10.1016/0890-5401(92)90008-4
[31]
Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: a compositionally verified compiler for a higher-order imperative language. In ICFP. ACM, 166–178. https://doi.org/10.1145/2784731.2784764
[32]
Max S. New and Amal Ahmed. 2018. Graduality from embedding-projection pairs. Proc. ACM Program. Lang., 2, ICFP (2018), 73:1–73:30. https://doi.org/10.1145/3236768
[33]
Luca Padovani. 2010. Session Types = Intersection Types + Union Types. In ITRS (EPTCS, Vol. 45). 71–89. https://doi.org/10.4204/EPTCS.45.6
[34]
Marco Patrignani. 2020. Why Should Anyone use Colours? or, Syntax Highlighting Beyond Code Snippets. CoRR, abs/2001.11334 (2020), arxiv:2001.11334
[35]
Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, and Frank Piessens. 2015. Secure Compilation to Protected Module Architectures. ACM Trans. Program. Lang. Syst., 37, 2 (2015), 6:1–6:50. https://doi.org/10.1145/2699503
[36]
Daniel Patterson and Amal Ahmed. 2019. The next 700 compiler correctness theorems (functional pearl). Proc. ACM Program. Lang., 3, ICFP (2019), 85:1–85:29. https://doi.org/10.1145/3341689
[37]
Daniel Patterson, Noble Mushtak, Andrew Wagner, and Amal Ahmed. 2022. Semantic soundness for language interoperability. In PLDI. ACM, 609–624. https://doi.org/10.1145/3519939.3523703
[38]
Daniel Patterson, Jamie Perconti, Christos Dimoulas, and Amal Ahmed. 2017. FunTAL: reasonably mixing a functional language with assembly. In PLDI. ACM, 495–509. https://doi.org/10.1145/3062341.3062347
[39]
James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In ESOP (LNCS, Vol. 8410). Springer, 128–148. https://doi.org/10.1007/978-3-642-54833-8_8
[40]
Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, and Adam Chlipala. 2020. Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. In IJCAR (LNCS, Vol. 12167). 119–137. https://doi.org/10.1007/978-3-030-51054-1_7
[41]
Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, and Yuchen Fu. 2015. A Compositional Semantics for Verified Separate Compilation and Linking. In CPP. ACM, 3–14. https://doi.org/10.1145/2676724.2693167
[42]
Ingrid Rewitzky. 2003. Binary Multirelations. In Theory and Applications of Relational Structures as Knowledge Instruments (LNCS, Vol. 2929). Springer, 256–271. https://doi.org/10.1007/978-3-540-24615-2_12
[43]
A. W. Roscoe. 2010. Understanding Concurrent Systems. Springer. https://doi.org/10.1007/978-1-84882-258-0
[44]
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. 2022. Islaris: verification of machine code against authoritative ISA semantics. In PLDI. ACM, 825–840. https://doi.org/10.1145/3519939.3523434
[45]
Michael Sammler, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. 2023. DimSum: A Decentralized Approach to Multi-language Semantics and Verification (Appendix). https://doi.org/10.5281/zenodo.7306313 Project webpage:
[46]
Michael Sammler, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. 2023. DimSum: A Decentralized Approach to Multi-language Semantics and Verification (Coq development). https://doi.org/10.5281/zenodo.7306313 Project webpage:
[47]
Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur. 2020. CompCertM: CompCert with C-assembly linking and lightweight modular verification. Proc. ACM Program. Lang., 4, POPL (2020), 23:1–23:31. https://doi.org/10.1145/3371091
[48]
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer. 2023. Conditional Contextual Refinement. In POPL. ACM. https://doi.org/10.1145/3571232
[49]
Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David A. Basin. 2020. Igloo: soundly linking compositional refinement and separation logic for distributed system verification. Proc. ACM Program. Lang., 4, OOPSLA (2020), 152:1–152:31. https://doi.org/10.1145/3428220
[50]
Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In POPL. ACM, 275–287. https://doi.org/10.1145/2676726.2676985
[51]
Andrew S. Tanenbaum and Herbert Bos. 2014. Modern Operating Systems (4th ed.). Prentice Hall Press, USA. isbn:013359162X https://dl.acm.org/doi/book/10.5555/2655363
[52]
Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco. 2022. Layered and object-based game semantics. Proc. ACM Program. Lang., 6, POPL (2022), 1–32. https://doi.org/10.1145/3498703
[53]
Moshe Y. Vardi. 1995. Alternating Automata and Program Verification. In Computer Science Today (LNCS, Vol. 1000). Springer, 471–485. https://doi.org/10.1007/BFb0015261
[54]
Peng Wang, Santiago Cuellar, and Adam Chlipala. 2014. Compiler verification meets cross-language linking via data abstraction. In OOPSLA. ACM, 675–690. https://doi.org/10.1145/2660193.2660201
[55]
Yuting Wang, Pierre Wilke, and Zhong Shao. 2019. An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang., 3, POPL (2019), 62:1–62:30. https://doi.org/10.1145/3290375
[56]
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4, POPL (2020), 51:1–51:32. https://doi.org/10.1145/3371119

Cited By

View all
  • (2024)Extending the C/C++ Memory Model with Inline AssemblyProceedings of the ACM on Programming Languages10.1145/36897498:OOPSLA2(1081-1107)Online publication date: 8-Oct-2024
  • (2024)Refinement Composition LogicProceedings of the ACM on Programming Languages10.1145/36746458:ICFP(573-601)Online publication date: 15-Aug-2024
  • (2024)SECOMP: Formally Secure Compilation of Compartmentalized C ProgramsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3670288(1061-1075)Online publication date: 2-Dec-2024
  • Show More Cited By

Index Terms

  1. DimSum: A Decentralized Approach to Multi-language Semantics and Verification

      Recommendations

      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 7, Issue POPL
      January 2023
      2196 pages
      EISSN:2475-1421
      DOI:10.1145/3554308
      • Editor:
      Issue’s Table of Contents
      This work is licensed under a Creative Commons Attribution 4.0 International License.

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 11 January 2023
      Published in PACMPL Volume 7, Issue POPL

      Permissions

      Request permissions for this article.

      Check for updates

      Badges

      Author Tags

      1. Coq
      2. Iris
      3. compilers
      4. multi-language semantics
      5. non-determinism
      6. separation logic
      7. verification

      Qualifiers

      • Research-article

      Funding Sources

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)545
      • Downloads (Last 6 weeks)65
      Reflects downloads up to 21 Dec 2024

      Other Metrics

      Citations

      Cited By

      View all
      • (2024)Extending the C/C++ Memory Model with Inline AssemblyProceedings of the ACM on Programming Languages10.1145/36897498:OOPSLA2(1081-1107)Online publication date: 8-Oct-2024
      • (2024)Refinement Composition LogicProceedings of the ACM on Programming Languages10.1145/36746458:ICFP(573-601)Online publication date: 15-Aug-2024
      • (2024)SECOMP: Formally Secure Compilation of Compartmentalized C ProgramsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3670288(1061-1075)Online publication date: 2-Dec-2024
      • (2024)Securing Verified IO Programs Against Unverified Code in F*Proceedings of the ACM on Programming Languages10.1145/36329168:POPL(2226-2259)Online publication date: 5-Jan-2024
      • (2024)Fully Composable and Adequate Verified Compilation with Direct Refinements between Open ModulesProceedings of the ACM on Programming Languages10.1145/36329148:POPL(2160-2190)Online publication date: 5-Jan-2024
      • (2024)An Iris Instance for Verifying CompCert C ProgramsProceedings of the ACM on Programming Languages10.1145/36328488:POPL(148-174)Online publication date: 5-Jan-2024
      • (2023)Stuttering for FreeProceedings of the ACM on Programming Languages10.1145/36228577:OOPSLA2(1677-1704)Online publication date: 16-Oct-2023
      • (2023)Melocoton: A Program Logic for Verified Interoperability Between OCaml and CProceedings of the ACM on Programming Languages10.1145/36228237:OOPSLA2(716-744)Online publication date: 16-Oct-2023
      • (2023)Iris-Wasm: Robust and Modular Verification of WebAssembly ProgramsProceedings of the ACM on Programming Languages10.1145/35912657:PLDI(1096-1120)Online publication date: 6-Jun-2023

      View Options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Login options

      Full Access

      Media

      Figures

      Other

      Tables

      Share

      Share

      Share this Publication link

      Share on social media