基于非阻塞同步机制的多核并发系统模块化验证方法研究

非阻塞同步机制是当前多核处理器并行编程模式的基础，模块化验证方法通过验证代码的模块性和重用性，降低了验证的复杂度，提高了验证的效率，是实现细粒度、高并发量的多核并发系统性质验证的有效方法。然而，现有的模块化验证方法不能直接用来推理和验证基于非阻塞同步机制的多核并发系统的活性、安全性等时序性质。活性和安全性是并发系统的重要性质，无法对这些性质进行验证，也就无法保证系统的正确性。本课题针对这一重要问题，研究基于非阻塞同步机制的多核并发系统时序性质的模块化验证方法，重点关注如何模块化地推理和验证非阻塞同步机制的活性，扩展已有的用于非阻塞同步验证的 R-G推理到支持非阻塞同步时序性质验证的时序R-G推理，研究两种不同R-G推理的统一抽象描述，给出用于实现多种性质验证于一体的统一程序逻辑验证框架；进一步，探讨该方法在非阻塞同步机制多核并发算法中的应用，给出一系列验证实例。

基于多处理器系统的非阻塞同步机制的正确性验证是当前理论计算机研究领域的前沿热点问题。然而细粒度和高并发量使非阻塞同步机制的实现变得复杂且更易出错，给验证带来很大困难。现有的验证方法不能直接用来推理和验证基于非阻塞同步机制的并发数据结构的活性和安全性性质。活性和安全性是并发系统的重要性质，无法对这些性质进行验证，也就无法保证系统的正确性。本课题针对这一重要问题，研究并提出了基于非阻塞同步机制的并发数据结构的正确性验证方法。研究内容分为如下四个方面。..1．我们首先扩展投影时序逻辑框架使其支持带有原子块的并发程序设计结构，提出了一种并发时序逻辑程序设计模型(αPTL)。该新逻辑允许我们描述当代并发程序设计语言中的一些重要机制，如内存原语Compare-And-Swap，为基于非阻塞同步机制的程序书写，规范描述和验证提供了基础。..2．我们进一步研究基于R-G风格的模块化推理和验证并发数据结构安全性和活性的方法，给出了一个可靠的公理系统用于推理无锁（lock-free）性质，提出了用于模块化验证时序性质的统一程序逻辑验证框架。..3．另外，我们提出了基于并发对象互模拟的方法来验证并发数据结构正确性。这是在该领域第一次提出这种新颖的验证思路。该方法既可以验证可线性化性质，同时可以验证演进性质，弥补了传统的基于精化方法只能验证可线性化性质，不能保持演进性质的不足；另外，互模拟方法为并发数据结构的验证提供了多项式算法复杂度，相比于基于路径精化的模型检测方法（其复杂度是PSPACE-Complete），在验证执行效率上有了本质上的改进。..4．使用课题所研究的方法，完成了10个基于非阻塞同步机制的多核并发算法的验证实例，证明了可线性化性质和演进性质。..本课题的研究为基于非阻塞同步机制的并发数据结构的可线性化和演进性质的自动化验证提出了新方法，同时对多核并发系统中其他各种高级同步机制的验证和实现具有普遍意义和重要理论价值。