research-article

Open access

CompCertM: CompCert with C-assembly linking and lightweight modular verification

Authors:

Chung-Kil HurAuthors Info & Claims

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

Article No.: 23, Pages 1 - 31

https://doi.org/10.1145/3371091

Published: 20 December 2019 Publication History

Abstract

Supporting multi-language linking such as linking C and handwritten assembly modules in the verified compiler CompCert requires a more compositional verification technique than that used in CompCert just supporting separate compilation. The two extensions, CompCertX and Compositional CompCert, supporting multi-language linking take different approaches. The former simplifies the problem by imposing restrictions that the source modules should have no mutual dependence and be verified against certain well-behaved specifications. On the other hand, the latter develops a new verification technique that directly solves the problem but at the expense of significantly increasing the verification cost.

In this paper, we develop a novel lightweight verification technique, called RUSC (Refinement Under Self-related Contexts), and demonstrate how RUSC can solve the problem without any restrictions but still with low verification overhead. For this, we develop CompCertM, a full extension of the latest version of CompCert supporting multi-language linking. Moreover, we demonstrate the power of RUSC as a program verification technique by modularly verifying interesting programs consisting of C and handwritten assembly against their mathematical specifications.

Supplementary Material

WEBM File (a23-song.webm)

Download
70.12 MB

References

[1]

Andrew W. Appel. 2011. Verified Software Toolchain. In Proceedings of the 20th European Symposium on Programming (ESOP 2011).

[2]

Andrew W Appel. 2014. Program Logics for Certified Compilers. Cambridge University Press.

Digital Library

[3]

Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel. 2014. Verified Compilation for Shared-Memory C. In Proceedings of the 23rd European Symposium on Programming Languages and Systems (ESOP 2014).

Digital Library

[4]

Derek Dreyer, Georg Neis, and Lars Birkedal. 2010. The impact of higher-order state and control effects on local relational reasoning. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010).

Digital Library

[5]

Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, and David Costanzo. 2011. CertiKOS: A Certified Kernel for Secure Cloud Computing. In Proceedings of the 2nd ACM SIGOPS Asia-Pacific Workshop on Systems (APSys 2011).

Digital Library

[6]

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 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015).

Digital Library

[7]

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 Symposium on Operating Systems Design and Implementation (OSDI 2016).

[8]

Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. 2012. The Marriage of Bisimulations and Kripke Logical Relations. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012).

Digital Library

[9]

Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, and Xinyu Feng. 2019. Towards Certified Separate Compilation for Concurrent Programs. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019).

Digital Library

[10]

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxedmemory Concurrency. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017).

Digital Library

[11]

Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis. 2015. A formal C memory model supporting integer-pointer casts. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015).

Digital Library

[12]

Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2016. Lightweight Verification of Separate Compilation. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016).

Digital Library

[13]

Xavier Leroy. 2006. Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006).

Digital Library

[14]

Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM 52, 7 (July 2009), 107–115.

Digital Library

[15]

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 Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015).

Digital Library

[16]

Max S. New, William J. Bowman, and Amal Ahmed. 2016. Fully Abstract Compilation via Universal Embedding. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016).

Digital Library

[17]

Daniel Patterson and Amal Ahmed. 2019. The Next 700 Compiler Correctness Theorems (Functional Pearl). In Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming (ICFP 2019).

Digital Library

[18]

Daniel Patterson, Jamie Perconti, Christos Dimoulas, and Amal Ahmed. 2017. FunTAL: Reasonably Mixing a Functional Language with Assembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017).

Digital Library

[19]

James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In Proceedings of the 23rd European Symposium on Programming (ESOP 2014).

[20]

Gabriel Scherer, Max S. New, Nick Rioux, and Amal Ahmed. 2018. FabULous Interoperability for ML and a Linear Language. In Proceedings of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018).

[21]

Gordon Stewart. 2015. Verified Separate Compilation for C. Ph.D. Dissertation. Princeton University.

[22]

Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015).

[23]

Yuting Wang, Pierre Wilke, and Zhong Shao. 2019. An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code. In Proceedings of the 46th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2019).

Digital Library

Cited By

Song YLee D(2024)Refinement Composition LogicProceedings of the ACM on Programming Languages10.1145/36746458:ICFP(573-601)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674645
Zhang LWang YWu JKoenig JShao Z(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
https://dl.acm.org/doi/10.1145/3632914
Kim JGu RShao Z(2024) : A simplified and abstract multicore hardware model for large scale system software formal verification Journal of Systems Architecture10.1016/j.sysarc.2023.103049147(103049)Online publication date: Feb-2024
https://doi.org/10.1016/j.sysarc.2023.103049
Show More Cited By

Index Terms

CompCertM: CompCert with C-assembly linking and lightweight modular verification
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Software verification
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Lightweight verification of separate compilation
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Major compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the ...
Lightweight verification of separate compilation
POPL '16

Major compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the ...
Verified peephole optimizations for CompCert
PLDI '16

Transformations over assembly code are common in many compilers. These transformations are also some of the most bug-dense compiler components. Such bugs could be elim- inated by formally verifying the compiler, but state-of-the- art formally verified ...

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 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 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: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
1,086
Total Downloads

Downloads (Last 12 months)309
Downloads (Last 6 weeks)51

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Song YLee D(2024)Refinement Composition LogicProceedings of the ACM on Programming Languages10.1145/36746458:ICFP(573-601)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674645
Zhang LWang YWu JKoenig JShao Z(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
https://dl.acm.org/doi/10.1145/3632914
Kim JGu RShao Z(2024) : A simplified and abstract multicore hardware model for large scale system software formal verification Journal of Systems Architecture10.1016/j.sysarc.2023.103049147(103049)Online publication date: Feb-2024
https://doi.org/10.1016/j.sysarc.2023.103049
Kim JKoenig JChen HGu RShao Z(2024) : A template to build verified thread-local interfaces with software scheduler abstractions Journal of Systems Architecture10.1016/j.sysarc.2023.103046147(103046)Online publication date: Feb-2024
https://doi.org/10.1016/j.sysarc.2023.103046
Loitzl AZuleger F(2024)Modeling Register Pairs in CompCertIntegrated Formal Methods10.1007/978-3-031-76554-4_8(128-147)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_8
Cho MSong YLee DGäher LDreyer D(2023)Stuttering for FreeProceedings of the ACM on Programming Languages10.1145/36228577:OOPSLA2(1677-1704)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622857
Guéneau AHostert JSpies SSammler MBirkedal LDreyer D(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
https://dl.acm.org/doi/10.1145/3622823
Sewell TMyreen MTan YKumar RMihajlovic AAbrahamsson OOwens S(2023)Cakes That Bake Cakes: Dynamic Computation in CakeMLProceedings of the ACM on Programming Languages10.1145/35912667:PLDI(1121-1144)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591266
Song YCho MLee DHur CSammler MDreyer D(2023)Conditional Contextual RefinementProceedings of the ACM on Programming Languages10.1145/35712327:POPL(1121-1151)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571232
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
Show More Cited By

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