Authors
- Youngju Song, Seoul National University, Korea
- Minki Cho, Seoul National University, Korea
- Dongjoo Kim, Seoul National University, Korea
- Yonghyun Kim, Seoul National University, Korea
- Jeehoon Kang, KAIST, Korea
- Chung-Kil Hur*, Seoul National University, Korea
* Hur is the corresponding author.
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.