基于TL2软件事务内存的并发程序的精化验证

Refinement-Based Verification of TL2 Transactions

软件事务内存并发机制将对共享存储复杂的同步访问控制转嫁给底层系统开发者,从而大大减轻高层程序员开发并发程序的负担。TL2是一个经典的基于锁的高性能软件事务内存算法。本文以一个TL2读写事务的底层具体实现为验证目标,首先采用并发程序间的精化关系来刻画基于TL2的底层细粒度并发程序是某个具体的高层抽象原子事务代码块的正确实现,然后通过基于依赖保证的并发程序模拟技术证明两个程序间具有精化关系,完成读写事务的底层实现在代码级的验证并总结TL2算法满足的不变式,为完成TL2算法在代码级的完整验证奠定基础。

Software transactional memory （STM） concurrent mechanism successfully moves the complex control of simultaneous access to shared memory into the runtime system （which is handled by STM algorithm developers） and thus greatly reduces the burden on high-level programmers to develop concurrent programs. This paper aims to verify a concrete read-write transaction implemented with TL2 algorithm, which is a classic lock- based high-performance software transactional memory algorithm. First a refinement relation between concurrent programs is used to describe that the low-level fine-grained TL2-based code is a correct implementation of a specific high-level abstract atomic transaction code block. Then the refinement relation between the two programs is proved by the rely-guarantee-based simulation. Also, a representative TL2-based example is verified at the code level. The invariants of TL2 algorithm are summarized. The above work lays the foundation for complete verification of the TL2 algorithm in code level.