CAJ | 학술논문

软件事务内存并发机制将对共享存储复杂的同步访问控制转嫁给底层系统开发者，从而大大减轻高层程序员开发并发程序的负担。TL2是一个经典的基于锁的高性能软件事务内存算法。本文以一个TL2读写事务的底层具体实现为验证目标，首先采用并发程序间的精化关系来刻画基于TL2的底层细粒度并发程序是某个具体的高层抽象原子事务代码块的正确实现，然后通过基于依赖保证的并发程序模拟技术证明两个程序间具有精化关系，完成读写事务的底层实现在代码级的验证并总结TL2算法满足的不变式，为完成TL2算法在代码级的完整验证奠定基础。
연건사무내존병발궤제장대공향존저복잡적동보방문공제전가급저층계통개발자，종이대대감경고층정서원개발병발정서적부담。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.