一句话：提出轻量级验证技术 RUSC，使 CompCert 在无限制条件下支持 C 与手写汇编的多语言链接，且验证开销低。
CompCert 原本只支持分离编译，要支持 C 与手写汇编模块的多语言链接，就需要比其现有方法更具组合性的验证技术。已有工作采取两种路线：CompCertX 通过限制源模块之间不得相互依赖、且须满足特定良行为规约来简化问题；Compositional CompCert 则直接给出新的验证技术，但代价是验证成本大幅上升。本文提出一种新的轻量级验证技术 RUSC（Refinement Under Self-related Contexts），在没有任何上述限制的前提下解决该问题，同时保持较低的验证开销。作者据此实现了 CompCertM，即最新版 CompCert 的完整扩展，支持多语言链接。此外，作者通过对由 C 与手写汇编组成的有趣程序按其数学规约进行模块化验证，展示了 RUSC 作为程序验证技术的能力。
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.
@article{paperbot576,
title = {CompCertM: CompCert with C-assembly linking and lightweight modular verification},
author = {Youngju Song and Minki Cho and Dongjoo Kim and Yonghyun Kim and Jeehoon Kang and Chung-Kil Hur},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371091}
}