验证组合编译的统一语义接口的自底向上方法
摘要：已验证的组合编译（Verified compositional compilation，VCC）是一种支持异构程序编译的模块化验证编译的概念。实现VCC的关键在于设计一个语义接口，使得能够对编译单个模块的正确性定理进行组合。现有的大多数VCC技术会从一开始就确定一个语义接口，并将其应用于每个编译传递过程。这会对现有框架进行重大改变，并且使得理解语义接口强制的条件与编译传递实际要求之间的关系变得困难。另一种方法是为各个编译传递过程设计合适的语义接口，并将它们组合成一个统一的接口，以准确反映底层编译传递的要求。然而，这需要具有垂直可组合模拟关系，即使对编译验证框架进行了广泛的改变，这在传统上被认为非常困难。 我们提出了一种自底向上的方法来构建VCC的统一语义接口的解决方案。我们的起点是CompCertO，这是一种支持VCC的CompCert（最先进的验证编译器）扩展，但缺乏统一接口。我们发现CompCertO中的CompCert Kripke逻辑关系（CKLR）为模块之间的演变内存状态提供了统一的内存保护概念，并且是可传递组合的。基于这个统一和可组合的CKLR，我们将CompCertO中所有编译传递过程（除了三个值分析传递过程）的模拟关系合并到一个统一的接口中。通过将其应用于验证具有互递归的非平凡异构程序的组合编译，我们展示了这个统一接口的简洁性和有效性。
作者：Ling Zhang, Yuting Wang, J''er''emie Koenig, Zhong Shao
论文ID：2302.12990
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-03-21