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