面对多核处理器技术的不断革新,为充分地利用多核资源提升程序的性能,设计和实现高并发的数据结构变得越来越重要。为获得更多的并发和更好的性能,程序开发者会尽可能的采用细粒度同步技术来实现并发数据结构。然而这些数据结构通常复杂灵巧、易出错、可靠性难以保证。因此,形式化验证并发数据结构对提高并发软件的可靠性和安全性有着重要意义。可线性化是一个主流的并发数据结构安全性标准。本文针对并发数据结构可线性化标准及其验证方法方面进行了深入研究。本文分析了可线性化标准的局限性,在此基础上提出了强可线性化标准。验证并发数据结构强可线性化最困难的部分还是验证可线性化。正如Khyzha所说的一样,尽管有大量的可线性化验证技术,要验证复杂并发数据结构的可线性化仍是一项极具挑战性的任务。本文致力于提供简单易用的方法验证并发数据结构的可线性化,具体做了如下几个方面的工作:（1）本文首先分析了可线性化的二个局限性:1)可线性化给用户带来的是观察精化的保证,而不是观察等价的保证;2)即使客户端以和并发数据结构方法非交互的方式直接访问数据结构,可线性化的观察精化保证也会被破坏。针对以上二个局限,提出了并发数据结构的强一致性标准—强可线性化,并证明了强可线性化蕴含观察等价和即使在一个允许客户端以兼容的方式直接访问数据结构的程序模型下,强可线性化的观察等价保证也不会被破坏。本文选择客户端的执行路径作为客户的观察行为,这不仅使得客户能够观察到客户端程序的最终状态,也使得客户能够观察到相关的时态属性。对于强可线性化的一种特例,即并发数据结构的实现和规约有相同状态空间的强可线性化（称这个规约为顺序规约）,本文揭示了并发数据结构相对顺序规约的强可线性化与相对其它抽象模型的强可线性化之间的联系。直观上讲,顺序规约可视为并发数据结构最大化的原子抽象,即要证明一个并发数据结构相对一个更抽象的模型是强可线性化的,可简化证明顺序规约和这个抽象模型的相关联系。因为顺序规约和这个抽象模型的方法都是原子的,显然证明后者比证明前者容易的多。（2）提出了基于抽象约简的可线性化验证方法,并应用该方法验证了MS无锁队列、DGLM队列、HSY栈、数据对快照（Pair Snapshot）、基于惰性链表的集合（Lazy Set）、基于乐观锁的集合（the Optimistic List）等这些灵巧复杂的并发数据结构。本文提出的基于抽象约简的可线性化验证方法与其它基于Lipton约简的可线性化验证方法不同之处在于:1)基于抽象的约简仅要求满足抽象语义的子路径是可约简的,而不要求整个路径是可约简的;2)把路径约简从单路径扩展到双路径;3)对于不可约简的读方法,通过可达性证明把读方法转化成一个可达点,可线性化证明化简到证明写方法与可达点的约简性。总之,基于抽象约简的可线性化验证方法既保持了Lipton约简的简单、直观、易用性,同时也将Lipton约简方法应用到更多复杂灵巧的数据结构中。（3）对于一个可线性化的并发数据结构的封装扩展,证明了要验证这个扩展后的并发数据结构的可线性化,可证明由抽象方法代替它里面的具体方法后生成的并发数据结构的可线性化。因为抽象方法都是原子的,证明后者要比验证前者容易的多。依据这个结论,本文使用基于抽象约简的可线性化验证方法验证了一个基于封装扩展的并发哈希表。（4）对于一个采用抵消优化机制的并发栈,证明了只要正常的并发执行（即非抵消优化机制参与的并发执行部分）是可线性化的,那么并发栈就是可线性化的。利用这个结论,可以简化采用抵消优化机制的并发栈的可线性化证明。（5）提出了基于先于偏序关系属性的并发队列和并发栈的可线性化验证方法,并证明了它们是完备的。该方法将并发队列/栈的可线性化证明化简到验证入队/栈操作与出队/栈操作间的先于偏序关系属性,并发数据结构的设计与实现者容易快速的掌握和应用这个方法。本文应用这两个方法验证了HW队列（the Herlihy-Wing queue）、时间戳队列（the Time-Stamped queue）、篮式队列（Baskets Queue）、LCRQ队列和时间戳栈（the Time-Stamped stack）等这些基于抽象约简方法不能处理的、极具挑战性的并发数据结构。