并发程序的精化验证技术及其关键应用

Program refinement has been used as a theoretical foundation for program verification, including algorithm verification, compiler verification and OS kernel verification. However, existing theories and verification techniques all have serious problems to work in a concurrent setting. In particular, they either lack compositionality, or cannot reason about termination and liveness properties of programs. Also, most of the theories are built upon the idealized sequentially consistent memory model with vanilla threads. They cannot support relaxed memory models, or interrupt and event-driven concurrency model. Another problem is the lack of Hoare-style axiomatic proof theory and tools. This makes verification a very challenging job. In this project we would like to develop new theories and verification techniques for concurrent program refinement, and use it as a uniform framework for concurrency verification. Our work is based on existing compositional verification techniques, but we extend them to support liveness verification. We plan to develop new specification and simulation theories for refinement proofs in relaxed memory models and interrupt-driven concurrency. We will also propose new relational program logic as a proof theory, and build corresponding tools to automate the verification process. To demonstrate the applicability of our work, we will apply them in three key applications, including verification of fine-grained concurrent algorithms, verification of software transactional memory (STM) implementations as a special compiler, and verification of interrupt handlers and thread schedulers in OS kernels.

精化验证是一种重要的程序验证技术，它在算法验证、编译器验证和操作系统验证等方向都有着重要的应用。然而，在并发环境下，现有的精化验证理论和技术尚有着很多缺陷，不能有效支持上述的应用需求，具体表现为活性验证需求和验证技术的可组合性无法兼顾、缺少对弱内存模型和带中断的并发等多种并发模型的支持、以及缺少公理化的证明理论和工具等。 针对上述不足，本课题研究并发程序的精化验证理论和技术，在坚持验证技术的模块化和可组合性的基础上，探讨在不同并发模型下的精化关系刻画和证明，加强对程序活性验证的支持，开发霍尔风格的公理化程序逻辑和证明系统，最终形成支持多种并发程序验证的统一的基础验证理论和框架。我们还将探讨该理论和框架在细粒度并发算法验证、软件事务型内存算法（一种并发编译技术）验证以及操作系统内核中的中断和调度机制验证方面的应用，以检验理论和框架的有效性和实用性。

精化验证是一种重要的程序验证技术，它在算法验证、编译器验证和操作系统验证等方向都有着重要的应用。然而，在并发环境下，现有的精化验证理论和技术尚有着很多缺陷，不能有效支持上述的应用需求，具体表现为活性验证需求和验证技术的可组合性无法兼顾、缺少对弱内存模型和带中断的并发等多种并发模型的支持、以及缺少公理化的证明理论和工具等。.. 针对上述不足，本课题研究并发程序的精化验证理论和技术。我们研究不同并发模型下的精化关系的刻画和证明，给出TSO内存模型下的rely/guarantee程序逻辑，以及支持硬件中断和抢占式并发的底层并发模型的精化关系刻画和程序逻辑；深入研究并发对象的终止性和进展性（progress）的刻画和验证，以及与之相等价的上下文精化理论，不仅支持无等待、无锁、无饿死、无死锁等经典进展性定义的验证，还针对带阻塞方法的并发对象，首次提出了“部分无饿死”和“部分无死锁”这两种新的进展性定义，并给出了新的抽象规约，以及支持进展性验证的程序逻辑。.. 我们还成功将相关理论应用于细粒度并发算法验证、并发编译验证、以及操作系统内核中的中断和调度机制验证等。实际应用包括对一系列细粒度并发算法的进展性验证（验证的算法包括Michael-Scott队列算法、DGLM队列算法、Synchronous queue算法、Lock-coupling List、Lazy List、Optimistic List、以及各种锁的实现等），将经典的软件事务型内存算法TL2刻画为程序变换并使用精化验证技术验证其正确性；对并发C程序编译器的模块化验证；以及对嵌入式实时操作系统内核μC/OS-II的关键模块的验证。这些关键领域的应用表明了我们的精化验证理论的有效性和实用性。