多线程程序中关联变量原子性验证关键技术研究

发布时间：2017-07-30 04:18

  本文关键词：多线程程序中关联变量原子性验证关键技术研究

  更多相关文章： 关联变量 原子性验证 多线程程序序符号执行 一般图可达性 指针别名分析 并行干扰插值

【摘要】：多线程程序中关联变量的原子性是指在共享内存的并行模型中,保证具有一定关联关系的共享变量集合,在任意的并行执行顺序访问条件下,其所满足的关联关系仍然成立的一种性质。该性质是多线程程序设计过程必须满足的约束之一,是保证多线程程序安全性的核心因素,是并行程序安全运行的重要前提。同时,随着多核硬件环境的日益普及,越来越多的软件通过并行化充分利用已有的计算资源以提高软件系统的性能,尤其在航天、武器和医疗等安全攸关领域有着广泛的应用。因此,验证并行程序中关联变量原子性的研究对保障并行程序的质量安全具有重要意义。本文主要对验证条件和验证过程所涉及的关键技术进行研究,首先研究验证条件的确定问题即确认验证目标,本文主要是要确定保持原子性的关联变量集合,重点解决原子性关联变量和一般关联变量混淆的问题。其次,研究如何判断程序是否满足验证条件即验证过程的问题,本文采取根据程序可达状态来进行判断的策略,先从决定程序可达状态的控制依赖和数据依赖角度出发,分别研究了面向变量访问次序判别的图可达性问题和指针别名分析问题,然后在此基础上研究了可达状态约策略问题。在图可达性问题中,具体解决非树边传递闭包计算问题、环子图查询和非结构化区域解析问题。在别名分析问题中,具体解决按需策略下分析精度不足的问题。在可达状态约简策略问题中,重点改善了并行程序可达状态粒度过粗导致约简效率低的问题,提出了并行干扰插值结构和基于此的并行程序符号执行算法,重点提高可达程序状态间通过蕴含关系合并的可能性并完善轮询语句完备性分析,进而实现对多线程程序原子性的高效验证。首先,对于关联变量提取问题,在验证条件中的关联变量挖掘与提取方面,针对现有面向原子性验证的关联变量提取方法误报率高的问题,提出了基于程序依赖图约简的关联变量挖掘与提取算法。通过简化程序控制依赖图中控制流图信息来泛化变量间非依赖性顺序的关联关系,然后利用频繁子图挖掘算法挖掘关联变量候选集合,最终通过过滤策略提取需要保持原子性的关联变量集合。实验中经人工确认,与现有基于频繁项挖掘的提取方法相比,该方法具有更低的关联变量误报率。然后,在验证阶段的控制流图可达性判断研究方面:(1)对于一般图可达性分析,针对一般图可达性算法缺少对程序控制流图中非树边和循环体内有向环子图的优化与处理问题,提出了一种层次线性化编码索引模式,利用控制流图中区域结构所隐含的层次顺序关系,建立表达多重从属关系的可达性索引。该编码不仅能够避免计算有向图非生成树边的可达性传递闭包,而且整合了程序控制流图中有向环子图的编码与图可达性判断,进而提高可达性判断效率。(2)对于指针别名分析问题,针对当前程序控制流图结构化方法难以满足程序分析的流敏感精度要求的问题,提出了程序控制流图的虚拟区域结构。通过分析匹配分支节点列表和结构化区域的对应关系,提出了一种非结构化区域内虚拟区域的构造方法,该方法根据未匹配分支节点列表冲突来增加虚拟汇聚结点,进而构造非结构化区域内虚拟区域。该方法不仅能够恢复非结构区域内隐含的区域结构,而且还保留了非结构化区域中原有各语句间的相对位置关系,提高了结构化方法的流敏感分析精度。其次,在验证阶段的指针别名分析方面,针对当前基于上下文无关文法的按需别名分析方法只具有流不敏感精度的问题,提出了流敏感精度的按需别名分析算法,将别名关系查询问题统一转换为对特定变量赋值实例在控制流可达条件下赋值路径的搜索问题,以实现流敏感的按需别名分析。实验表明,与流不敏感的按需别名分析相比,该方法可以在保证查询效率的前提下,有效提高按需别名分析的精度。最后,在并行程序可达状态计算方面,针对当前基于干扰的有界模型检测中限制搜索踪迹长度导致的不完备性问题和严重的计算负担问题,提出了面向多线程程序原子性验证的符号执行方法,该方法以约束逻辑程序为实现基础,利用并行干扰插值结构对多线程程序可达状态空间进行搜索。该结构对全局线程间调度进行过估计(Over-Approximate)、局部线程内不可行踪迹泛化、并行可达状态泛化三个层次递进的对并行线程间的交叠执行状态进行抽象,实现了快速的状态空间约简,缓解了处理循环体时对代表性踪迹的完全展开导致的严重计算负担问题,同时保证了并行验证的完备性。上述方法的提出,有效解决了多线程程序中关联变量原子性验证中的关键问题,为提高并行程序安全性验证的自动化程度、效率和准确性,以及提高并行软件质量奠定了理论基础。
【关键词】：关联变量 原子性验证 多线程程序序符号执行 一般图可达性 指针别名分析 并行干扰插值
【学位授予单位】：哈尔滨工业大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：TP391.41
【目录】：

• 摘要4-6
• Abstract6-15
• 第1章 绪论15-33
• 1.1 课题来源15
• 1.2 课题背景及研究的目的和意义15-17
• 1.3 国内外的研究现状及分析17-29
• 1.3.1 关联变量挖掘研究现状分析17-19
• 1.3.2 控制流图分析研究现状分析19-23
• 1.3.3 指针分析研究现状分析23-25
• 1.3.4 并行程序原子性违背缺陷检测及验证研究现状分析25-29
• 1.4 主要研究内容29-33
• 第2章 多线程程序中关联变量挖掘与提取33-54
• 2.1 引言33-34
• 2.2 支持多程序语言的静态信息提取方法34-40
• 2.2.1 与静态信息提取相关的GCC源代码分析34-35
• 2.2.2 静态信息提取35-39
• 2.2.3 实验结果与分析39-40
• 2.3 保持原子性的多线程关联变量的特点分析40-43
• 2.3.1 关联变量语义分析40-41
• 2.3.2 关联变量行为分析41-43
• 2.4 基于程序依赖图的关联变量挖掘与提取43-48
• 2.4.1 原子性关联变量集合的关联关系分析43-44
• 2.4.2 挖掘算法概要44
• 2.4.3 约简的程序依赖图44-45
• 2.4.4 程序依赖图预处理45-46
• 2.4.5 频繁子图挖掘46-47
• 2.4.6 多线程关联变量提取与过滤47-48
• 2.5 实验及分析48-53
• 2.6 本章小结53-54
• 第3章 面向变量访问次序判别的图可达性分析54-100
• 3.1 引言54-55
• 3.2 结构化控制流图可达性分析55-77
• 3.2.1 层次线性化编码域56-62
• 3.2.2 层次线性化编码规则62-67
• 3.2.3 基于LLC的CFG可达性判断67-73
• 3.2.4 实验与分析73-77
• 3.3 非结构化控制流图的虚拟区域77-99
• 3.3.1 结构化区域的分析80-86
• 3.3.2 虚拟分支 -会合节点匹配对的恢复算法86-92
• 3.3.3 虚拟区域在非结构化区域图可达性应用92-96
• 3.3.4 实验与分析96-99
• 3.4 本章小结99-100
• 第4章 流敏感精度的按需指针别名分析100-115
• 4.1 引言100-101
• 4.2 流敏感对别名分析精度的影响分析101-103
• 4.2.1 按需别名分析101-102
• 4.2.2 流敏感信息的表达102-103
• 4.3 流敏感信息的按需查询103-104
• 4.4 赋值流图104-106
• 4.5 赋值流搜索106-109
• 4.6 流敏感按需别名分析算法109-111
• 4.7 实验与分析111-114
• 4.7.1 流敏感精度的按需别名分析与指向分析方法对比111
• 4.7.2 按需别名分析的流敏感精度方法与流不敏感精度方法对比111-112
• 4.7.3 按需流敏感别名分析中搜索边数统计与分析112-114
• 4.8 本章小结114-115
• 第5章 基于并行干扰插值的多线程程序原子性验证115-139
• 5.1 引言115-117
• 5.2 相关概念117-119
• 5.2.1 程序执行顺序117-118
• 5.2.2 程序执行踪迹的操作语义118-119
• 5.2.3 克雷格插值119
• 5.3 并行程序的符号分析119-121
• 5.3.1 并行干扰与调度120
• 5.3.2 并行执行顺序的约束120
• 5.3.3 并行变迁的推导树120-121
• 5.4 并行干扰插值121-133
• 5.4.1 执行顺序偏序关系插值121-124
• 5.4.2 调度插值124-129
• 5.4.3 并行状态插值129-133
• 5.5 算法描述133-135
• 5.6 实验与分析135-137
• 5.7 本章小结137-139
• 结论139-141
• 参考文献141-152
• 攻读博士学位期间发表的学术论文152-154
• 致谢154-155
• 个人简历155

，

本文编号：592490