弱内存程序的形式语义模型及分析与验证技术研究

Weak memory programs (i.e. programs assuming weak memory models) allow various out of order executions, therefore often exhibiting sophisticated counterintuitive behaviors. It remains an extremely challenging problem as to how to better understand and characterize sophisticated semantic behaviors of weak memory programs and how to analyze and verify their correctness. The state of the art research in this area is still very much in its infancy, with a lot of open challenges. To tackle some of the challenges, this project aims to construct complete formal semantic models as well as advanced verification and analysis techniques for C11 weak memory programs. It will focus on semantic theories based on Hoare and He’s Unifying Theories of Programming (UTP), explore cutting-edge techniques in higher order separation logic, and construct comprehensive verification techniques for C11 weak memory programs. In this project we will (1) define UTP formal semantics for C11 weak memory programs, so as to avoid the ambiguity caused by informal semantics and to help users understand the semantic behaviors of weak memory programs more easily and correctly, (2) construct an advanced verification logic for C11 weak memory programs, based on higher order separation logic, that can be used to verify memory safety and functional correctness of such programs, (3) encode formal semantics and verification systems in Coq and construct mechanized Coq proofs for the soundness of the verification system, to ensure the reliability of the verification results, and (4) search for advanced static analysis techniques that can help improve the applicability and level of automation of the proposed verification system. In addition to theoretical studies, we will also build prototype tools on analysis and verification for C11 weak memory programs and conduct experimental case studies.

由于允许指令重排序等优化执行策略，弱内存程序通常表现出各种反直觉的复杂语义行为。如何正确理解和刻画这类程序的行为并验证其正确性是极具挑战性的前沿课题。国际上对弱内存程序的形式语义及分析与验证等方面的研究仍处于起步阶段，很多问题亟待解决。本项目的研究目标是为C11弱内存程序构建完整的形式语义模型以及分析与验证逻辑系统。首次研究基于程序统一理论（UTP）的弱内存语义模型，重点关注基于高阶分离逻辑的前沿技术，创建 C11完整验证逻辑系统。本项目的研究重点在于：（1）定义C11弱内存程序的UTP语义模型，以有效避免非形式语义带来的歧义性，帮助用户正确理解其语义行为；（2）构建C11弱内存程序的验证逻辑，用于内存安全性和功能正确性的验证；（3）为语义模型和验证系统提供机械化的认证，以保证分析与验证结果的可靠性；（4）设计用于弱内存程序的高级静态分析方法，提高验证系统的可用性和自动化程度。

弱内存程序由于允许指令重排序等优化策略，通常表现出各种反直觉的复杂语义行为。如何正确理解和刻画这类程序的行为并验证其正确性是极具挑战性的前沿课题。本项目研究弱内存程序的形式化分析与验证的理论与技术。首先，为了刻画弱内存程序的语义行为，本项目定义了具有精细控制力度的形式语义模型。在形式语义模型基础上，本项目研究弱内存程序验证等逻辑与推理技术，构建了基于高阶逻辑的程序验证系统，并证明了已构建的程序验证系统的可靠性，接着，本项目结合模型学习、数据精化、机器学习等技术，提出了支持不同特性的自动验证算法。最后，为了提高验证系统的可用性和自动化程度，本项目设计了不同应用场景的高级静态分析方法。本项目不仅为弱内存程序的分析和验证提供一套行之有效的形式化方法和理论框架，而且还实现了一套原型工具集，有望进一步实际应用中的程序分析和验证。本项目的研究不仅对程序语言原理、形式验证等具有积极意义，而且有助于提高实际应用中的软件质量。