近年来,由于物理定律的障碍,使用增加晶体管数量来提高处理器性能的摩尔定律已经逐渐走到了尽头。为了解决这个问题,人们将目光投向了多核处理器,它主要通过并行计算来提高性能。多核多处理等新一代系统结构对并行的全面支持,引发了软件开发方式上的巨变。软件不再能从硬件性能提升中免费获益,而需要充分利用硬件特性实现并发,才能充分发挥新一代硬件的优势。因此,面向多核时代的编程人员,越来越需要设计和开发并行程序,以充分利用这种多核硬件特征。然而,并行编程是有相当难度的。一方面,目前的语言和工具仍没有做好将应用转化为并行程序的准备;另一方面,并行编程要求程序员以人类难以适应的方式思考。在并行编程中,对共享资源的并发访问控制是一个关键性的问题。传统上,程序员通常使用锁机制来进行并发控制,但是传统的锁机制存在以下缺陷:1)粒度选择困难,粗粒度锁编程简单但并发度低;细粒度锁能提高并发度但是难以实现,2)不具有组合性,两段使用锁机制实现的、能正确运行的代码合并后得到的代码可能出现错误,3)容易引起优先级倒置、护送、死锁等问题。为了给程序员提供一种易编程同时具有高并发度的并行编程机制,研究人员将数据库中的并发控制概念引入到编程语言中形成事务内存系统。事务内存主要分为两层:在高层,它提供一种比较简单的类似串行形式的程序语义使得编程容易;在低层,研究人员使用锁等机制设计各种不同的细粒度并发系统来将高层的程序翻译到底层系统中并发地执行。通过这两层系统,可以有效地解决长久以来并行编程给程序员带来的诸多困扰。但是,事务内存系统的出现也给并行程序验证带来了新的挑战,已有的并行验证技术与逻辑系统不能直接用来验证事务内存程序。因此,本学位论文中的工作着眼于此问题,通过深入研究软件事务内存系统的各种实现机制,并结合现有的并行程序验证技术,设计了一种新的用于验证软件事务内存程序的逻辑推理系统。通过验证软件事务内存程序来指导事务内存系统的实现,为构造高可信并行软件奠定基础。同时,本文还关注一些现有的软件事务内存系统实现算法,使用形式化方法来验证该实现算法的安全性与正确性。本文的主要工作和贡献可以分为以下几个部分:·在携带基础证明程序的基础上设计了一种用于验证基于事务内存同步机制的汇编级并行程序的程序逻辑系统。在该系统中,本文巧妙地设计了一种结合了并发分离逻辑和携权限分离逻辑的程序逻辑来支持验证事务代码中的投机读操作。此外,基于该系统本文中还提出了一种验证事务代码原子性的方法,以保证事务代码执行的正确性。·在定理辅助证明工具Coq中完成了本文所设计的验证事务内存程序逻辑系统的所有可靠性证明,从而将该逻辑系统中的验证推理规则从受信任计算基础中排除出去,使其具有更高的可靠性。此外,我们通过具体的实例证明来体现此逻辑系统的有效性与实用性。·使用最新的程序逻辑验证了一种经典的软件事务内存实现算法Transac-tional Locking II的安全性与正确性。在证明中,通过使用辅助变量与辅助代码,本文总结出一种验证基于版本化锁实现的事务投机读操作的方法。此外,本文还证明了基于该实现算法生成的事务代码与对应高层程序之间的一致性。