近日，上海交通大学电子信息与电气工程学院约翰·霍普克罗夫特计算机科学中心长聘教轨副教授汪宇霆团队在程序设计语言领域编译验证方向取得重要进展，研究成果“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://popl22.sigplan.org/details/POPL-2022-popl-research-papers/25/Verified-Compilation-of-C-Programs-with-a-Nominal-Memory-Model

汪宇霆，电院长聘教轨副教授，此前于美国耶鲁大学计算机系担任博士后研究员，博士毕业于美国明尼苏达大学双城分校。长期从事形式化方法方面研究，内容涵盖形式化验证和程序设计语言的理论基础（包括证明论、类型论、逻辑框架等）以及它们在关键性系统软件（如编译器和操作系统）中的应用，代表性研究成果以发表于形式化验证和程序设计语言的顶级国际会议（如POPL、CAV、OOPSLA、ESOP等）。此外，还致力于开发基于证明理论的定理证明工具，作为主要设计人员之一参与开发了基于高阶抽象语法的新型定理证明工具Abella（http://abella-prover.org），其已被成功应用于程序设计语言学术界的多个研究项目。