基于软件事务内存的并行程序验证

论文摘要

近年来,由于物理定律的障碍,使用增加晶体管数量来提高处理器性能的摩尔定律已经逐渐走到了尽头。为了解决这个问题,人们将目光投向了多核处理器,它主要通过并行计算来提高性能。多核多处理等新一代系统结构对并行的全面支持,引发了软件开发方式上的巨变。软件不再能从硬件性能提升中免费获益,而需要充分利用硬件特性实现并发,才能充分发挥新一代硬件的优势。因此,面向多核时代的编程人员,越来越需要设计和开发并行程序,以充分利用这种多核硬件特征。然而,并行编程是有相当难度的。一方面,目前的语言和工具仍没有做好将应用转化为并行程序的准备;另一方面,并行编程要求程序员以人类难以适应的方式思考。在并行编程中,对共享资源的并发访问控制是一个关键性的问题。传统上,程序员通常使用锁机制来进行并发控制,但是传统的锁机制存在以下缺陷:1)粒度选择困难,粗粒度锁编程简单但并发度低;细粒度锁能提高并发度但是难以实现,2)不具有组合性,两段使用锁机制实现的、能正确运行的代码合并后得到的代码可能出现错误,3)容易引起优先级倒置、护送、死锁等问题。为了给程序员提供一种易编程同时具有高并发度的并行编程机制,研究人员将数据库中的并发控制概念引入到编程语言中形成事务内存系统。事务内存主要分为两层:在高层,它提供一种比较简单的类似串行形式的程序语义使得编程容易;在低层,研究人员使用锁等机制设计各种不同的细粒度并发系统来将高层的程序翻译到底层系统中并发地执行。通过这两层系统,可以有效地解决长久以来并行编程给程序员带来的诸多困扰。但是,事务内存系统的出现也给并行程序验证带来了新的挑战,已有的并行验证技术与逻辑系统不能直接用来验证事务内存程序。因此,本学位论文中的工作着眼于此问题,通过深入研究软件事务内存系统的各种实现机制,并结合现有的并行程序验证技术,设计了一种新的用于验证软件事务内存程序的逻辑推理系统。通过验证软件事务内存程序来指导事务内存系统的实现,为构造高可信并行软件奠定基础。同时,本文还关注一些现有的软件事务内存系统实现算法,使用形式化方法来验证该实现算法的安全性与正确性。本文的主要工作和贡献可以分为以下几个部分:·在携带基础证明程序的基础上设计了一种用于验证基于事务内存同步机制的汇编级并行程序的程序逻辑系统。在该系统中,本文巧妙地设计了一种结合了并发分离逻辑和携权限分离逻辑的程序逻辑来支持验证事务代码中的投机读操作。此外,基于该系统本文中还提出了一种验证事务代码原子性的方法,以保证事务代码执行的正确性。·在定理辅助证明工具Coq中完成了本文所设计的验证事务内存程序逻辑系统的所有可靠性证明,从而将该逻辑系统中的验证推理规则从受信任计算基础中排除出去,使其具有更高的可靠性。此外,我们通过具体的实例证明来体现此逻辑系统的有效性与实用性。·使用最新的程序逻辑验证了一种经典的软件事务内存实现算法Transac-tional Locking II的安全性与正确性。在证明中,通过使用辅助变量与辅助代码,本文总结出一种验证基于版本化锁实现的事务投机读操作的方法。此外,本文还证明了基于该实现算法生成的事务代码与对应高层程序之间的一致性。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 研究背景
• 1.2 携证明代码（PCC）
• 1.3 并行程序验证
• 1.4 事务内存简介
• 1.4.1 事务内存的实现机制
• 1.4.2 事务内存的语义研究
• 1.5 本文概述
• 1.5.1 研究工作
• 1.5.2 主要创新和贡献
• 1.5.3 章节安排
• 第2章 程序验证技术
• 2.1 汇编语言验证系统（CAP）
• 2.2 基于共享内存的并发技术
• 2.2.1 同步机制
• 2.3 通用并行语言
• 2.3.1 变量
• 2.3.2 断言
• 2.4 Rely-Guarantee方法
• 2.4.1 推理规则
• 2.5 分离逻辑
• 2.5.1 抽象分离逻辑
• 2.5.2 分离逻辑实例
• 2.5.3 并发分离逻辑
• 2.5.4 携权限分离逻辑
• 2.6 Local Rely-Guarantee 逻辑
• 第3章 软件事务内存程序逻辑系统
• 3.1 抽象机器模型
• 3.2 断言语言
• 3.2.1 描述共享堆的断言语言
• 3.2.2 描述线程状态的断言语言
• 3.3 程序规范
• 3.3.1 程序规范语言
• 3.3.2 推理规则
• 3.3.3 可靠性
• 3.3.4 逻辑系统应用
• 3.4 原子性验证
• 3.4.1 弱原子性中的异常行为
• 3.4.2 形式化验证
• 3.4.3 实例证明
• 3.5 本章小结
• 第4章 TL2实现算法验证
• 4.1 TL2实现算法介绍
• 4.2 细粒度并发程序验证
• 4.2.1 辅助变量与代码
• 4.2.2 带辅助变量的证明示例
• 4.3 TL2算法中的辅助变量与代码
• 4.4 形式化验证
• 4.5 本章小结
• 第5章 结束语
• 5.1 论文工作总结
• 5.2 进一步的工作
• 参考文献
• 致谢
• 在读期间发表的学术论文与取得的研究成果