Verified compositional compilation (VCC) is a notion of modular verification of compilers that supports compilation of heterogeneous programs. The key to achieve VCC is to design a semantic interface that enables composition of correctness theorems for compiling individual modules. Most of the existing techniques for VCC fix a semantic interface from the very beginning and force it down to every single compiler pass. This requires significant changes to the existing framework and makes it difficult to understand the relationship between conditions enforced by the semantic interface and the actual requirements of compiler passes. A different approach is to design appropriate semantic interfaces for individual compiler passes and combine them into a unified interface which faithfully reflects the requirements of underlying compiler passes. However, this requires vertically composable simulation relations, which were traditionally considered very difficult to construct even with extensive changes to compiler verification frameworks. We propose a solution to construction of unified semantic interfaces for VCC with a bottom-up approach. Our starting point is CompCertO, an extension of CompCert -- the state-of-the-art verified compiler -- that supports VCC but lacks a unified interface. We discover that a CompCert Kripke Logical Relation (CKLR) in CompCertO provides a uniform notion of memory protection for evolving memory states across modules and is transitively composable. Based on this uniform and composable CKLR, we then merge the simulation relations for all the compiler pass in CompCertO (except for three value analysis passes) into a unified interface. We demonstrate the conciseness and effectiveness of this unified interface by applying it to verify the compositional compilation of a non-trivial heterogeneous program with mutual recursion.


翻译:验证组合编译(VCC)是一种支持异构程序编译的模块化编译器验证概念。实现VCC的关键是设计一个语义接口,使得能够组合编译单个模块的正确性定理。大多数现有的VCC技术从一开始就固定了一个语义接口,并将其强行应用到每个编译器通路。这需要对现有框架进行重大改变,并使得理解语义接口所强制的条件与实际编译器通路需求之间的关系变得困难。另一种方法是针对各个编译器通路设计适当的语义接口,并将它们组合成一个统一接口,以忠实地反映底层编译器通路的要求。然而,这需要可纵向组合的模拟关系,即使在对编译器验证框架进行大量更改的情况下,这也被传统上认为是非常困难的。我们提出了一种自下而上的方法来构建用于VCC的统一语义接口的解决方案。我们的出发点是CompCertO,它是CompCert的扩展,支持VCC但缺乏统一接口。我们发现CompCert Kripke Logical Relation(CKLR)在CompCertO中为跨模块不断演变的存储状态提供了一致的内存保护概念,并且是可传递组合的。基于这个具有一致性和可组合性的CKLR,我们将CompCertO中所有编译器通路的模拟关系(除了三个值分析通路)合并成一个统一接口。我们通过将其应用于验证一个非平凡异构程序的组合编译来证明这个统一接口的简洁性和有效性。

0
下载
关闭预览

相关内容

编译器(Compiler),是一种计算机程序,它会将用某种编程语言写成的源代码(原始语言),转换成另一种编程语言(目标语言)。
分布式图神经知识表示框架
专知会员服务
61+阅读 · 2020年7月28日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
30+阅读 · 2019年10月17日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
深度自进化聚类:Deep Self-Evolution Clustering
我爱读PAMI
15+阅读 · 2019年4月13日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
全球人工智能
19+阅读 · 2017年12月17日
【推荐】ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
机器学习研究会
20+阅读 · 2017年12月17日
【推荐】用Python/OpenCV实现增强现实
机器学习研究会
14+阅读 · 2017年11月16日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
13+阅读 · 2017年12月5日
VIP会员
相关VIP内容
分布式图神经知识表示框架
专知会员服务
61+阅读 · 2020年7月28日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
30+阅读 · 2019年10月17日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
相关资讯
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
深度自进化聚类:Deep Self-Evolution Clustering
我爱读PAMI
15+阅读 · 2019年4月13日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
全球人工智能
19+阅读 · 2017年12月17日
【推荐】ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
机器学习研究会
20+阅读 · 2017年12月17日
【推荐】用Python/OpenCV实现增强现实
机器学习研究会
14+阅读 · 2017年11月16日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员