中国团队在程序设计语言领域编译验证方向取得重要进展

近日，上海交通大学电子信息与电气工程学院约翰·霍普克罗夫特计算机科学中心长聘教轨副教授汪宇霆团队在程序设计语言领域编译验证方向取得重要进展，研究成果“Verified Compilation of C Programs with a Nominal Memory Model”已被程序设计语言领域顶级会议ACM SIGPLAN Symposium on Principles of Programming Languages （POPL 2022）接收。该项目由上海交通大学与耶鲁大学共同完成，上海交通大学为第一完成单位，汪宇霆为第一作者。该研究创新性地将名义技术（Nominal Techniques）中命名和支持集合（Support）的概念引入传统的基于区块的内存模型，提出了一种称为名义内存模型（Nominal Memory Model）的新型内存模型，将其成功应用于C程序编译验证。

POPL是程序设计语言领域历史最久、水平最高的国际会议，也是中国计算机协会（CCF）推荐A类会议。会议主要关注程序语言和编程系统的基本原则和重要创新，内容涵盖程序语言设计，程序分析，程序验证，编译器技术等具体领域。POPL每年有中国科研机构参与的论文仅1-3篇，以第一单位完成的论文则更加难得，2022年全球范围仅录取65篇。

编译验证是通过形式化方法构建可信软件的重要一环。由于源程序需要经过编译之后才能被计算机执行，因此只有验证了编译器的正确性，即编译产生的目标程序能够保存源程序的语义，才能保证源程序在实际运行时正确工作。

在命令式语言（如C/C++/Java）的编译验证中，内存模型作为程序语义的核心组成部分起着至关重要的作用。汪宇霆团队注意到已有的编译验证工作中对内存模型的实现，特别是对于内存空间的表述存在很大的局限性，这不仅导致了编译验证中额外的负担，更阻碍了对于模块化和并发程序的语义描述和验证。

基于上述观察进行研究，该团队创新性地将名义技术（Nominal Techniques）中命名和支持集合（Support）的概念引入传统的基于区块的内存模型，提出了一种称为名义内存模型（Nominal Memory Model）的新型内存模型。相对于传统的内存模型，名义内存模型为满足抽象命名接口的各类内存空间给出统一形式表述，从而提供了一套对不同内存结构和程序语义进行编译验证的统一框架。

该团队在最先进的经验证C语言编译器CompCert中实现了名义内存模型，并基于此完成了CompCert中全部编译过程的证明，得到了首个支持抽象内存空间的CompCert扩展，即NominalCompCert。并以此为基础进一步开发了多个CompCert扩展版本，分别简化了关键编译步骤的验证难度和提供了更好的对并发程序语义以及模块化验证的支持（如图所示）。这些工作为实现针对模块化并发程序的灵活、可扩展编译验证打下了坚实的基础，并有望被进一步用于改进程序验证领域内基于传统内存模型的其他工作。获取更多前沿科技 研究进展 访问：https://byteclicks.com