近年来,随着超线程、多核体系结构等多线程技术的发展和广泛应用,计算机硬件已经提供了越来越高效的软件运行平台。但是要更好地利用这些平台的并行优势,计算机软件就需要具备更好地并行性,以充分利用多个处理器的性能。并行程序已经成为了软件开发的主流。然而要确保顺序程序的正确性已经是非常困难的了,要保证并行程序的正确性难度更甚。这是因为在并行程序中,程序员还需要处理共享数据的并发存取问题,确保数据在不同线程中的有效性。传统上,程序员使用锁的方式来管理并行程序中共享数据的并发存取。但是锁方式不仅难于推理,而且还容易出现死锁等导致程序进入异常执行状态的隐患。为减轻程序员开发并行程序的负担,提高软件开发的效率,近年的研究提出了使用事务内存同步机制来管理共享数据的并发存取。提供了事务内存同步机制的系统通过自动地管理数据的并发访问,免除了程序员在这方面的负担,也避免了死锁等锁机制的致命隐患。但是近年来围绕着事务内存同步机制的研究主要集中于提供事务内存同步机制的系统的各种实现策略及其性能的提高上,而对该同步机制在程序推理、形式验证及易于推理方面的研究甚少。针对事务内存同步机制相关研究的现状,基于程序推理验证的研究成果,本文提出了一种推理方法以推理使用了事务内存同步机制的实现系统所提供的编程结构的程序。该推理方法基于众所周知的不变式证明(Invariance Proof)方法并对Hoare逻辑进行了扩展,通过指明共享数据上的不变式来约束多个线程间的并发访问,可靠、可行,并具备模块化验证的特点。同时,本文还专注于事务内存同步机制的语义研究,在携带证明的代码的研究的基础上,将所提出的推理方法形式化到遵循事务内存同步机制语义的Hoare风格的验证框架中,并证明了推理方法遵循事务内存同步机制的语义的可靠性。此外,本文还给出了推理验证的应用实例,展示了本文所提出的推理方法和验证框架的有效性。最后,本文通过详尽的比较,阐明了事务内存同步机制相对于传统的锁同步机制易推理的优点,展示了事务内存同步机制对程序推理的简化。本文的主要特色和贡献为:·本文提出了一种Hoare风格的推理方法,用于在事务内存同步机制的语义的高层抽象上推理源语言级的并行程序。·本文也提出了一个携带证明的代码(Proof-Carrying Code)风格的验证框架,用于在事务内存同步机制的语义的底层实现上验证汇编级的并行程序,并证明了验证框架遵循事务内存同步机制的语义的可靠性。该验证框架的提出,填补了携带证明的代码的研究在事务内存同步机制方面的空白。·本文在Coq定理证明辅助工具中完成了所提出的验证框架的可靠性证明,从而将验证框架中的验证推理系统从受信任计算基础中排除出去,使得本文的验证框架具有更高的可靠性。·本文还通过详细的比较阐述了事务内存同步机制相对于锁同步机制的易推理的优势。