Refinement-Based Verification Of TL2Transactions

With the wide application of multicore processors, concurrent programming becomes a indispensable software development technique, which brings programmers a big challenge. Traditional concurrent programming uses locking mechanism to ensure mutual exclusive accesses to shared resources, but the performance of coarse-grained locks is poor. Fine-grained locks perform better, but are complicated to use and error-prone. Writing simple and efficient code using fine-grained locks is very difficult and may easily lead to deadlocks, priority inversion and other issues. Software transactional memory (STM) 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 reduce the burden on high-level programmers to develop concurrent programs, but the algorithms for STM are often subtly designed and their implementations are error-prone. Therefore, since it is a part of the system software, formal verification of the correctness of its implementation is of great significance to improve the reliability and the security of concurrent softwares.There are many different strategies to implement the Software transactional memory algorithm. Existing research shows that lock-based STM algorithm has obvious advantages in terms of performance. This article aims to verify TL2, 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 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, two representative TL2-based examples are verified. The invariants of TL2algorithm are summarized. The above work lays the foundation for complete verification of the TL2algorithm.The main contributions of this article are as follows:(1) We apply the rely-guarantee-based simulation to verify implementations of two representative transactions. One is a read-write transaction whose read-set and write-set intersect, and the other is a read-only transaction. We verify that the TL2-based low-level fine-grained codes refine the high-level abstract atomic transaction code.(2) We show the correspondence between the concrete state of the TL2-based low-level fine-grained code and the abstract state of the atomic transaction code. We also show the invariants specifying the correspondence. Our work lays the foundation for the complete verification of the TL2algorithm.