随着多核处理器的广泛应用,并发编程成为软件开发的主流方式,但是并发编程给程序员带来了很大的挑战。传统的并发编程主要是用锁机制来保证共享资源的互斥访问,锁机制是一种常用的同步手段。但是粗粒度锁性能较差；而细粒度锁性能较好,但使用过于复杂,容易出错,编写简单高效的代码非常困难,容易导致死锁和优先级倒置等问题。软件事务内存(STM)并发机制将对共享存储复杂的同步访问控制转嫁给底层系统开发者,从而大大减轻高层程序员开发并发程序的负担,但是STM并发机制往往设计得十分精妙,在实现时极易出错。因而它作为系统软件的一部分,形式化验证其实现的正确性对提高并发软件的可靠性和安全性有着重要意义。STM算法在实现策略上有多种不同的选择方式,已有的研究工作表明基于锁的STM算法在性能上具有明显优势。本文以一个经典的基于锁的高性能STM算法TL2为验证目标,首先采用并发程序间的精化关系来刻画基于TL2的底层细粒度代码是某个具体的高层抽象原子事务代码块的正确实现,然后通过基于依赖保证的并发程序模拟技术证明两个程序间具有精化关系,完成基于TL2算法的两个有代表性的具体实例的验证,总结TL2算法满足的不变式,为完成TL2算法的完整验证奠定基础。本文的主要贡献如下：(1)应用基于依赖保证的模拟技术验证了读集和写集相交、只读的两个典型事务的底层实现,即验证基于TL2的底层细粒度实现是对高层抽象原子事务代码的精化。(2)给出了TL2算法中底层细粒度程序执行具体状态和原子事务执行的抽象状态对应关系,并给出了两者对应关系满足的不变式,为完成整个TL2算法的形式化验证奠定了基础。