A Compositional Semantics for Verified Separate Compilation and Linking
A Compositional Semantics for Verified Separate Compilation and Linking
复制标题
用于验证单独编译和链接的组合语义
DOI：
10.1145/2676724.2693167
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Yuchen Fu
中科院分区：
文献类型：
--
作者：
T. Ramananandro;Zhong Shao;Shu;Jérémie Koenig;Yuchen Fu
最近的突破性的努力，如CompCert已经取得了令人信服的情况下，机械化验证的编译器正确性的现实C程序是可行的和实用的。不幸的是，现有的验证编译器只能处理整个程序-这严重限制了它们的适用性，并阻止了验证C程序与验证外部库的链接。在本文中，我们提出了一种新的组合语义推理开放模块，并支持验证单独的编译和链接。更具体地说，我们用行为语义中的显式事件替换外部函数调用。然后，我们开发了一个经过验证的链接操作符，它通过将每个外部函数调用事件替换为模拟所请求函数的行为来对（潜在反应）行为进行惰性替换。最后，我们将展示如何应用我们的新语义来构建一个支持垂直组合和水平组合的细化基础设施。
Recent ground-breaking efforts such as CompCert have made a convincing case that mechanized verification of the compiler correctness for realistic C programs is both viable and practical. Unfortunately, existing verified compilers can only handle whole programs---this severely limits their applicability and prevents the linking of verified C programs with verified external libraries. In this paper, we present a novel compositional semantics for reasoning about open modules and for supporting verified separate compilation and linking. More specifically, we replace external function calls with explicit events in the behavioral semantics. We then develop a verified linking operator that makes lazy substitutions on (potentially reacting) behaviors by replacing each external function call event with a behavior simulating the requested function. Finally, we show how our new semantics can be applied to build a refinement infrastructure that supports both vertical composition and horizontal composition.