并发数据结构无锁实现的验证方法研究

并发数据结构无锁实现被广泛应用在系统和库等底层支撑软件的开发中，从而使得运行在多核处理器上的并发软件从中获益。提高并发软件的可靠性需要研究这类程序的验证方法，正确的无锁实现要求同时具有部分正确性、终止性和原子性。然而目前大多数验证方法只考虑部分正确性验证，很少关注终止性验证，而关于原子性的验证方法更多针对的是使用锁的并发程序。.本项目拟提出一个程序逻辑验证并发数据结构无锁实现的部分正确性和终止性，并基于该程序逻辑设计一种逻辑关系进一步支持原子性验证。针对无锁实现本身的特点，程序逻辑在断言表达力和模块化推理的结合上更进一步，从而简化推理过程，具有较好的一般性和实用性；逻辑关系支持在可配置的上下文环境下的模块化推理，具有组合性和通用性。我们将应用提出的程序逻辑和逻辑关系来验证一些并发数据结构的无锁实现算法。

本项目按照项目计划书的要求执行，从并发数据结构无锁实现的正确性形式化定义出发，将并发数据结构无锁实现的正确性验证看作是一种特殊的并发程序变换的正确性验证，提出了一种新的并发程序变换的正确性验证方法，并将该方法应用在并发程序验证的多个方面，取得了一些被国际同行认可的成果。通过开展本项目的研究工作，共撰写论文9篇，在国际期刊和会议上发表的学术论文7篇，其中CCF推荐的A类期刊和会议论文2篇，值得一提的是，其中一篇会议论文发表在39届程序语言理论的顶级国际会议POPL上，此前中国大陆无任何单位以第一作者单位的身份在POPL上发表过论文。本项目负责人与合作导师一起培养了博士生一名，硕士生一名。总体而言，整个项目的执行情况良好，达到了预期的指标。