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

• Published in: Proceedings of ACM on programming languages 2020-01, Vol.4 (POPL), p.1-31
• Main Authors: Song, Youngju, Cho, Minki, Kim, Dongjoo, Kim, Yonghyun, Kang, Jeehoon, Hur, Chung-Kil
• Format: Article
• Language: English
• ISSN: 2475-1421; 2475-1421
• DOI: 10.1145/3371091

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.