低级并行代码中几种同步机制的验证
发布时间：2021-05-16 02:51
多核多处理器等以共享存储为特征的新一代系统结构的出现,加速了对快速研发基于共享资源的并行软件的需求,这给基于共享资源的高可信并行软件构造带来许多挑战性研究课题。在基于共享资源的并行软件构造中,线程间的交互和通信主要通过访问共享资源来实现,对共享资源访问的同步控制是保证并行程序正确执行的关键所在。目前用于共享变量的访问控制的同步机制主要有锁和事务内存两种。传统的同步机制通过锁保护的临界区来管理并行程序中的共享资源的并发存取,使用锁的方式不仅限制了程序在多核处理器上的执行效率,而且容易出现死锁等导致程序进入异常执行状态的隐患。读写锁和可重入锁是锁同步机制的优化实现,其中读写锁允许多个线程对共享数据进行并发只读访问,而可重入锁则通过允许线程再次获得所持有的锁来避免自死锁。事务内存是近年来为发挥多核多处理等系统结构的优势而开展的新型同步技术研究,它试图通过允许一组存取共享内存的指令（称为事务）原子且隔离地执行来简化并行编程。本课题小组的研究方向是验证使用多种同步机制的并行程序正确性,本论文则重点关注如何验证使用读写锁和可重入锁这两种同步机制的低级并行代码的正确性,并探讨同时使用锁和事务内存混合...
【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校
【文章页数】：124 页
【学位级别】：博士
【文章目录】：
摘要
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 进一步的工作
参考文献
致谢
在读期间发表的学术论文与取得的研究成果
【参考文献】：
期刊论文
[1]Certifying Concurrent Programs Using Transactional Memory[J]. 李隆,张昱,陈意云,李勇. Journal of Computer Science & Technology. 2009(01)
[2]“可信软件基础研究”重大研究计划综述[J]. 刘克,单志广,王戟,何积丰,张兆田,秦玉文. 中国科学基金. 2008(03)
[3]高可信软件工程技术[J]. 陈火旺,王戟,董威. 电子学报. 2003(S1)
[4]模型检测:理论、方法与应用[J]. 林惠民,张文辉. 电子学报. 2002(S1)
[5]并发程序验证的时序Petri网方法[J]. 丁志军,蒋昌俊. 计算机学报. 2002(05)
[6]PVM并行程序验证系统的原理与实现[J]. 张兆庆,蒋昌俊,乔如良,叶志宝,周杰. 计算机学报. 1999(04)
本文编号：3188825
【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校
【文章页数】：124 页
【学位级别】：博士
【文章目录】：
摘要
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 进一步的工作
参考文献
致谢
在读期间发表的学术论文与取得的研究成果
【参考文献】：
期刊论文
[1]Certifying Concurrent Programs Using Transactional Memory[J]. 李隆,张昱,陈意云,李勇. Journal of Computer Science & Technology. 2009(01)
[2]“可信软件基础研究”重大研究计划综述[J]. 刘克,单志广,王戟,何积丰,张兆田,秦玉文. 中国科学基金. 2008(03)
[3]高可信软件工程技术[J]. 陈火旺,王戟,董威. 电子学报. 2003(S1)
[4]模型检测:理论、方法与应用[J]. 林惠民,张文辉. 电子学报. 2002(S1)
[5]并发程序验证的时序Petri网方法[J]. 丁志军,蒋昌俊. 计算机学报. 2002(05)
[6]PVM并行程序验证系统的原理与实现[J]. 张兆庆,蒋昌俊,乔如良,叶志宝,周杰. 计算机学报. 1999(04)
本文编号：3188825
本文链接：https://www.wllwen.com/kejilunwen/jisuanjikexuelunwen/3188825.html
