低级并行代码中几种同步机制的验证

论文摘要

多核多处理器等以共享存储为特征的新一代系统结构的出现,加速了对快速研发基于共享资源的并行软件的需求,这给基于共享资源的高可信并行软件构造带来许多挑战性研究课题。在基于共享资源的并行软件构造中,线程间的交互和通信主要通过访问共享资源来实现,对共享资源访问的同步控制是保证并行程序正确执行的关键所在。目前用于共享变量的访问控制的同步机制主要有锁和事务内存两种。传统的同步机制通过锁保护的临界区来管理并行程序中的共享资源的并发存取,使用锁的方式不仅限制了程序在多核处理器上的执行效率,而且容易出现死锁等导致程序进入异常执行状态的隐患。读写锁和可重入锁是锁同步机制的优化实现,其中读写锁允许多个线程对共享数据进行并发只读访问,而可重入锁则通过允许线程再次获得所持有的锁来避免自死锁。事务内存是近年来为发挥多核多处理等系统结构的优势而开展的新型同步技术研究,它试图通过允许一组存取共享内存的指令（称为事务）原子且隔离地执行来简化并行编程。本课题小组的研究方向是验证使用多种同步机制的并行程序正确性,本论文则重点关注如何验证使用读写锁和可重入锁这两种同步机制的低级并行代码的正确性,并探讨同时使用锁和事务内存混合同步机制的并行程序的形式化验证方法。已有的形式化验证框架及程序逻辑在推理使用锁的并行程序的正确性时,多数只考虑语义简单的不可重入互斥锁,而不考虑读写锁和可重入锁,这些优化同步机制无疑可以提高并行程序的性能和易编程性,但由于其语义复杂,导致现有逻辑系统不能直接应用于推理它们。另外,锁和事务内存同步机制都有各自的优缺点,未来高性能并行软件可能需要同时使用它们而获得最大的性能收益,相应的高可信软件则要求设计程序逻辑保证同时使用它们的并行程序的正确性,而设计一种同时反映锁和事务内存同步机制特征的中间语言是推理混合同步机制的前提,而目前很少有研究工作考虑同时支持锁和事务内存同步机制的编程语言和程序逻辑的设计。针对锁和事务内存同步机制的研究现状以及已有程序验证方面的成果,本文的主要工作分为以下两个方面：一方面,在汇编语言级通过扩展邵中教授等提出的并发的经过证明的汇编编程（CCAP）验证框架,设计支持使用读写锁和可重入锁同步机制的并行程序正确性验证的Hoare风格专用程序逻辑,达到构造携带基础证明的程序（FPCC）的目标。我们选择模块性较好且适合于推理互斥临界区的并发分离逻辑作为所提出的验证框架的基础逻辑,并针对其在推理验证读写锁和可重入锁时的局限性分别进行了如下扩展：·通过扩展并发分离逻辑来支持以读写锁为基本同步原语的并行程序的推理,将并发分离逻辑中的分离扩展为“强分离”和“弱分离”两类,利用表示资源不相交的强分离描述写-写和读-写线程间对共享资源的划分,利用允许资源相交的弱分离描述读-读线程间对共享资源的划分,从而弥补并发分离逻辑中要求共享资源在多个并行线程间进行不相交的划分的不足。·在并发分离逻辑的基础上设计一种推理规则同时支持推理线程首次获得锁和再次获得锁的情况,避免资源被线程重复获得,从而使得并发分离逻辑能正确推理使用可重入锁的并行程序。我们用Coq定理证明辅助工具实现了所提出的验证框架及其可靠性证明,从而将验证框架中的验证推理系统从受信任计算基础中排除出去,使得本文的验证框架具有更高的可靠性。另一方面,提出一种新颖的语言构造“rev{C}”用于描述与事务内存实现特点密切相关的可逆代码块,得到一种中间语言将锁和事务融合在一个统一的编程模型中,并讨论了验证可逆代码块的困难及方法,为进一步深入研究可逆代码块的推理验证打下基础。通过实例说明该语法结构的表达能力,并阐述能安全执行的可逆代码块应该满足的基本安全属性。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景及相关工作
• 1.1.1 同步机制
• 1.1.2 并行程序正确性验证
• 1.2 存在的问题
• 1.3 本文的主要工作及贡献
• 1.4 章节安排
• 第二章 相关理论与技术基础
• 2.1 程序正确性检测方法
• 2.2 携带证明的代码（PCC）
• 2.3 同步技术基础
• 2.3.1 基本概念
• 2.3.2 各种同步机制的实现
• 2.4 并行程序验证技术
• 2.4.1 不变式证明技术
• 2.4.2 Rely-Guarantee推理
• 2.4.3 分离逻辑
• 2.4.4 并发分离逻辑（CSL）
• 2.4.5 结合R-G推理和分离逻辑（RGsep和SAGL）
• 2.4.6 局部R-G推理（LRG）
• 2.4.7 分析比较
• 2.5 CCAP验证框架
• 2.5.1 元逻辑
• 2.5.2 抽象机器
• 2.5.3 目标程序性质的证明框架
• 2.5.4 验证框架构造步骤
• 2.6 本章小结
• 第三章 使用读写锁的并行程序验证
• 3.1 问题描述
• 3.1.1 CSL的局限性
• 3.2 所有权转移推理方法
• 3.3 抽象机器
• 3.4 扩展并发分离逻辑
• 3.5 目标程序性质的证明框架
• 3.5.1 断言语言和规范语言的语法
• 3.5.2 推理规则
• 3.5.3 可靠性定理
• 3.6 目标代码验证举例
• 3.7 本章小结
• 第四章 使用可重入锁的并行程序验证
• 4.1 问题描述
• 4.2 抽象机器
• 4.3 目标程序性质的证明框架
• 4.3.1 断言语言和规范语言的语法
• 4.3.2 推理规则
• 4.3.3 可靠性定理
• 4.4 目标代码验证举例
• 4.5 本章小结
• 第五章 验证框架的Coq实现
• 5.1 抽象机器在Coq中的描述
• 5.1.1 机器语法定义
• 5.1.2 机器操作语义定义
• 5.2 程序规范在Coq中的描述
• 5.3 强弱分离在Coq中的描述
• 5.4 推理规则在Coq中的描述
• 5.5 框架可靠性证明
• 5.6 本章小结
• 第六章 使用混合同步控制机制的并行程序验证
• 6.1 问题描述
• 6.2 支持可逆代码块的并行语言
• 6.2.1 可逆代码块"rev{C}"
• 6.2.2 语法
• 6.2.3 程序实例
• 6.3 验证可逆代码块中的问题
• 6.3.1 操作语义
• 6.3.2 推理规则
• 6.4 本章小结
• 第七章 结束语
• 7.1 论文工作总结
• 7.2 进一步的工作
• 参考文献
• 致谢
• 在读期间发表的学术论文与取得的研究成果