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

《多线程程序中关联变量原子性验证关键技术研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、工学博士学位论文多线程程序中关联变量原子性验证关键技术研究RESEARCHONKEYTECHNIQUESOFMULTITHREADEDPROGRAMVERIFICATIONFORATOMICITYOFCORRELATEDVARIABLES哈尔滨工业大学2015年6月国内图书分类号：TP391学校代码：10213国际图书分类号：004.9密级：公开工学博士学位论文多线程程序中关联变量原子性验证关键技术研究博士研究生：逄龙导师：苏小红教授申请学位：工学博士学科：计算机科学与技术所在单位：计算机科学与技

2、术学院答辩日期：2015年6月授予学位单位：哈尔滨工业大学ClassifiedIndex:TP391U.D.C:004.9DissertationfortheDoctoralDegreeinEngineeringARESEARCHONKEYTECHNIQUESOFMULTITHREADEDPROGRAMVERIFICATIONFORATOMICITYOFCORRELATEDVARIABLESCandidate：PangLongSupervisor：ProfessorSuXiaohongAcadem

3、icDegreeAppliedfor：DoctorofEngineeringSpeciality：ComputerScienceandTechnologySchoolofComputerScienceandAffiliation：TechnologyDateofDefence：June2015Degree-Conferring-HarbinInstituteofTechnologyInstitution：哈尔滨工业大学工学博士学位论文摘要多线程程序中关联变量的原子性是指在共享内存的并行模型中，保证

4、具有一定关联关系的共享变量集合，在任意的并行执行顺序访问条件下，其所满足的关联关系仍然成立的一种性质。该性质是多线程程序设计过程必须满足的约束之一，是保证多线程程序安全性的核心因素，是并行程序安全运行的重要前提。同时，随着多核硬件环境的日益普及，越来越多的软件通过并行化充分利用已有的计算资源以提高软件系统的性能，尤其在航天、武器和医疗等安全攸关领域有着广泛的应用。因此，验证并行程序中关联变量原子性的研究对保障并行程序的质量安全具有重要意义。本文主要对验证条件和验证过程所涉及的关键技术进行研究，首先

5、研究验证条件的确定问题即确认验证目标，本文主要是要确定保持原子性的关联变量集合，重点解决原子性关联变量和一般关联变量混淆的问题。其次，研究如何判断程序是否满足验证条件即验证过程的问题，本文采取根据程序可达状态来进行判断的策略，先从决定程序可达状态的控制依赖和数据依赖角度出发，分别研究了面向变量访问次序判别的图可达性问题和指针别名分析问题，然后在此基础上研究了可达状态约策略问题。在图可达性问题中，具体解决非树边传递闭包计算问题、环子图查询和非结构化区域解析问题。在别名分析问题中，具体解决按需策略下分

6、析精度不足的问题。在可达状态约简策略问题中，重点改善了并行程序可达状态粒度过粗导致约简效率低的问题，提出了并行干扰插值结构和基于此的并行程序符号执行算法，重点提高可达程序状态间通过蕴含关系合并的可能性并完善轮询语句完备性分析，进而实现对多线程程序原子性的高效验证。首先，对于关联变量提取问题，在验证条件中的关联变量挖掘与提取方面，针对现有面向原子性验证的关联变量提取方法误报率高的问题，提出了基于程序依赖图约简的关联变量挖掘与提取算法。通过简化程序控制依赖图中控制流图信息来泛化变量间非依赖性顺序的关联

7、关系，然后利用频繁子图挖掘算法挖掘关联变量候选集合，最终通过过滤策略提取需要保持原子性的关联变量集合。实验中经人工确认，与现有基于频繁项挖掘的提取方法相比，该方法具有更低的关联变量误报率。然后，在验证阶段的控制流图可达性判断研究方面：-II-摘要(1)对于一般图可达性分析，针对一般图可达性算法缺少对程序控制流图中非树边和循环体内有向环子图的优化与处理问题，提出了一种层次线性化编码索引模式，利用控制流图中区域结构所隐含的层次顺序关系，建立表达多重从属关系的可达性索引。该编码不仅能够避免计算有向图非生

8、成树边的可达性传递闭包，而且整合了程序控制流图中有向环子图的编码与图可达性判断，进而提高可达性判断效率。(2)对于指针别名分析问题，针对当前程序控制流图结构化方法难以满足程序分析的流敏感精度要求的问题，提出了程序控制流图的虚拟区域结构。通过分析匹配分支节点列表和结构化区域的对应关系，提出了一种非结构化区域内虚拟区域的构造方法，该方法根据未匹配分支节点列表冲突来增加虚拟汇聚结点，进而构造非结构化区域内虚拟区域。该方法不仅能够恢复非结构区域内隐含的区域结构，而且还保留了非结构化区域中原